From 9d77dec344287d4ad42e723abfa5777dc3d01afc Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 20 Nov 2023 11:59:44 +0200
Subject: [PATCH] Move abs refine to BaseInvariant

---
 src/analyses/base.ml          | 43 ++++++++---------------------------
 src/analyses/baseInvariant.ml | 27 ++++++++++++++++++++++
 2 files changed, 36 insertions(+), 34 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 4911b0d033..f25f0a9693 100644
--- 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
index 72e00efbb1..a99e25e7c6 100644
--- 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