Move abs refine to BaseInvariant

goblint · Nov 20, 2023 · 9d77dec · 9d77dec
1 parent 8ea9ffa
commit 9d77dec
Show file tree

Hide file tree

Showing 2 changed files with 36 additions and 34 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -1753,40 +1753,15 @@ struct
   let branch ctx (exp:exp) (tv:bool) : store =
     let valu = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp in
     let refine () =
-      let refine0 =
-        let res = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global 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 (Analyses.ask_of_ctx ctx) ctx.global res e tv
-        | _ -> res
-      in
-      (* bodge for abs(...); To be removed once we have a clean solution *)
-      let refineAbs op absargexp valexp =
-        let flip op = match op with | Le -> Ge | Lt -> Gt | _ -> failwith "impossible" in
-        (* e.g. |arg| <= 40 *)
-        (* arg <= e  (arg <= 40) *)
-        let le = BinOp (op, absargexp, valexp, intType) in
-        (* arg >= -e  (arg >= -40) *)
-        let gt = BinOp(flip op, absargexp, UnOp (Neg, valexp, Cilfacade.typeOf valexp), intType) in
-        let one = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global refine0 le tv in
-        invariant ctx (Analyses.ask_of_ctx ctx) ctx.global one gt tv
-      in
-      match exp with
-      | BinOp ((Lt|Le) as op, CastE(t, Lval (Var v, NoOffset)), e,_) when tv ->
-        (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with 
-        | `Lifted (Abs arg) -> 
-          refineAbs op (CastE (t, arg)) e
-        | _ -> refine0)
-      | BinOp ((Lt|Le) as op, Lval (Var v, NoOffset), e, _) when tv ->
-        (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with 
-        | `Lifted (Abs arg) -> 
-          refineAbs op arg e
-        | _ -> refine0)
-      | _ -> refine0
+      let res = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global 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 (Analyses.ask_of_ctx ctx) ctx.global 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;
     (* First we want to see, if we can determine a dead branch: *)

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
@@ -821,4 +821,31 @@ struct
             FD.top_of fk
         in
         inv_exp (Float ftv) exp st
+
+  let invariant ctx a gs st exp tv: D.t =
+    let refine0 = invariant ctx a gs st exp tv in
+    (* bodge for abs(...); To be removed once we have a clean solution *)
+    let refineAbs op absargexp valexp =
+      let flip op = match op with | Le -> Ge | Lt -> Gt | _ -> failwith "impossible" in
+      (* e.g. |arg| <= 40 *)
+      (* arg <= e  (arg <= 40) *)
+      let le = BinOp (op, absargexp, valexp, intType) in
+      (* arg >= -e  (arg >= -40) *)
+      let gt = BinOp(flip op, absargexp, UnOp (Neg, valexp, Cilfacade.typeOf valexp), intType) in
+      let one = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global refine0 le tv in
+      invariant ctx (Analyses.ask_of_ctx ctx) ctx.global one gt tv
+    in
+    match exp with
+    | BinOp ((Lt|Le) as op, CastE(t, Lval (Var v, NoOffset)), e,_) when tv ->
+      (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with
+      | `Lifted (Abs arg) ->
+        refineAbs op (CastE (t, arg)) e
+      | _ -> refine0)
+    | BinOp ((Lt|Le) as op, Lval (Var v, NoOffset), e, _) when tv ->
+      (match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with
+      | `Lifted (Abs arg) ->
+        refineAbs op arg e
+      | _ -> refine0)
+    | _ -> refine0
+
 end