From b073b7189359a803d69a1f27b685ab5c4d5b8665 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 28 Dec 2023 11:42:28 +0200 Subject: [PATCH] Remove gs from invariant, invariant_fallback and refine_lv signatures --- src/analyses/base.ml | 8 ++++---- src/analyses/baseInvariant.ml | 14 +++++++------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 6448494305..3e22f2bfef 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1780,14 +1780,14 @@ struct let valu = eval_rv ~ctx exp in let refine () = let ask = Analyses.ask_of_ctx ctx in - let res = invariant ctx ask ctx.global ctx.local exp tv in + let res = invariant ctx ask ctx.local exp tv in if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.EqualSet exp)); if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a\n" d_exp exp Queries.ES.pretty (ctx.ask (Queries.CondVars exp)); if M.tracing then M.traceu "branch" "Invariant enforced!\n"; match ctx.ask (Queries.CondVars exp) with | s when Queries.ES.cardinal s = 1 -> let e = Queries.ES.choose s in - invariant ctx ask ctx.global res e tv + invariant ctx ask res e tv | _ -> res in if M.tracing then M.traceli "branch" ~subsys:["invariant"] "Evaluating branch for expression %a with value %a\n" d_exp exp VD.pretty valu; @@ -2034,7 +2034,7 @@ struct let assert_fn ctx e refine = (* make the state meet the assertion in the rest of the code *) if not refine then ctx.local else begin - let newst = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local e true in + let newst = invariant ctx (Analyses.ask_of_ctx ctx) ctx.local e true in (* if check_assert e newst <> `Lifted true then M.warn ~category:Assert ~msg:("Invariant \"" ^ expr ^ "\" does not stick.") (); *) newst @@ -2873,7 +2873,7 @@ struct in let module Unassume = BaseInvariant.Make (UnassumeEval) in try - Unassume.invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local e true + Unassume.invariant ctx (Analyses.ask_of_ctx ctx) ctx.local e true with Deadcode -> (* contradiction in unassume *) D.bot () in diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 51e71333f4..bd5bd7c6ed 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -91,8 +91,8 @@ struct then set a gs st addr t_lval value ~ctx (* no *_raw because this is not a real assignment *) else set a gs st addr t_lval new_val ~ctx (* no *_raw because this is not a real assignment *) - let refine_lv ctx a gs st c x c' pretty exp = - let set' lval v st = set a gs st (eval_lv ~ctx lval) (Cilfacade.typeOfLval lval) ~lval_raw:lval v ~ctx in + let refine_lv ctx a st c x c' pretty exp = + let set' lval v st = set a ctx.global st (eval_lv ~ctx lval) (Cilfacade.typeOfLval lval) ~lval_raw:lval v ~ctx in match x with | Var var, o when refine_entire_var -> (* For variables, this is done at to the level of entire variables to benefit e.g. from disjunctive struct domains *) @@ -120,7 +120,7 @@ struct set' x v st ) - let invariant_fallback ctx a (gs:V.t -> G.t) st exp tv = + let invariant_fallback ctx a st exp tv = (* We use a recursive helper function so that x != 0 is false can be handled * as x == 0 is true etc *) let rec helper (op: binop) (lval: lval) (value: VD.t) (tv: bool): (lval * VD.t) option = @@ -240,16 +240,16 @@ struct in match derived_invariant exp tv with | Some (lval, value) -> - refine_lv_fallback ctx a gs st lval value tv + refine_lv_fallback ctx a ctx.global st lval value tv | None -> if M.tracing then M.traceu "invariant" "Doing nothing.\n"; M.debug ~category:Analyzer "Invariant failed: expression \"%a\" not understood." d_exp exp; st - let invariant ctx a gs st exp tv: D.t = + let invariant ctx a st exp tv: D.t = let fallback reason st = if M.tracing then M.tracel "inv" "Can't handle %a.\n%t\n" d_plainexp exp reason; - invariant_fallback ctx a gs st exp tv + invariant_fallback ctx a st exp tv in (* inverse values for binary operation a `op` b == c *) (* ikind is the type of a for limiting ranges of the operands a, b. The only binops which can have different types for a, b are Shiftlt, Shiftrt (not handled below; don't use ikind to limit b there). *) @@ -696,7 +696,7 @@ struct | Float c -> invert_binary_op c FD.pretty (fun ik -> FD.to_int ik c) (fun fk -> FD.cast_to fk c) | _ -> failwith "unreachable") | Lval x, (Int _ | Float _ | Address _) -> (* meet x with c *) - let update_lval c x c' pretty = refine_lv ctx a gs st c x c' pretty exp in + let update_lval c x c' pretty = refine_lv ctx a st c x c' pretty exp in let t = Cil.unrollType (Cilfacade.typeOfLval x) in (* unroll type to deal with TNamed *) if M.tracing then M.trace "invSpecial" "invariant with Lval %a, c_typed %a, type %a\n" d_lval x VD.pretty c_typed d_type t; begin match c_typed with