Avoid subtraction in relational invariants

By moving terms and constant to other side.
goblint · Nov 29, 2024 · 44cc073 · 44cc073
1 parent cdb4322
commit 44cc073
Show file tree

Hide file tree

Showing 3 changed files with 38 additions and 34 deletions.
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -288,7 +288,7 @@ struct
       raise Unsupported_Linexpr1
 
   let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) =
-    let (const, _) = coeff_to_const ~scalewith false (Coeff.neg (Linexpr1.get_cst linexpr1)) in
+    let const = coeff_to_const ~scalewith true (Coeff.neg (Linexpr1.get_cst linexpr1)) in
     let terms = ref [] in
     let append_summand (c:Coeff.union_5) v =
       if not (Coeff.is_zero c) then
@@ -329,22 +329,26 @@ struct
     try
       let linexpr1 = Lincons1.get_linexpr1 lincons1 in
       let common_denominator = lcm_den linexpr1 in
-      let terms, const = cil_exp_of_linexpr1 ~scalewith:common_denominator linexpr1 in
-      let terms = List.sort [%ord: bool * CilType.Exp.t] terms in (* sort positive terms to be first *)
-      let lhs =
-        List.fold_left (fun acc (flip, term) ->
-            match acc, flip with
-            | None, false ->
-              Some term
-            | None, true ->
-              Some (UnOp (Neg, term, longlong))
-            | Some exp, _ ->
-              let op = if flip then MinusA else PlusA in
-              Some (BinOp (op, exp, term, longlong))
+      let terms, (const, constflip) = cil_exp_of_linexpr1 ~scalewith:common_denominator linexpr1 in
+      let (nterms, pterms) = List.partition fst terms in
+      let nterms = List.map snd nterms in
+      let pterms = List.map snd pterms in
+      let fold_terms terms =
+        List.fold_left (fun acc term ->
+            match acc with
+            | None -> Some term
+            | Some exp -> Some (BinOp (PlusA, exp, term, longlong))
           ) None terms
+        |> Option.default zero
+      in
+      let lhs = fold_terms pterms in
+      let rhs = fold_terms nterms in
+      let (lhs, rhs) =
+        if constflip then
+          BinOp (PlusA, lhs, const, longlong), rhs
+        else
+          lhs, BinOp (PlusA, rhs, const, longlong)
       in
-      let lhs = Option.default zero lhs in
-      let rhs = const in
       match Lincons1.get_typ lincons1 with
       | EQ -> Some (Cil.constFold false @@ BinOp(Eq, lhs, rhs, TInt(IInt,[])))
       | SUPEQ -> Some (Cil.constFold false @@ BinOp(Ge, lhs, rhs, TInt(IInt,[])))

diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t
@@ -29,7 +29,7 @@
       column: 3
       function: main
     location_invariant:
-      string: (long long )h - (long long )g == 0LL
+      string: (long long )h == (long long )g
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -40,7 +40,7 @@
       column: 3
       function: t_fun
     location_invariant:
-      string: (long long )h - (long long )g == 0LL
+      string: (long long )h == (long long )g
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -51,6 +51,6 @@
       column: 3
       function: t_fun
     location_invariant:
-      string: (long long )h - (long long )g == 0LL
+      string: (long long )h == (long long )g
       type: assertion
       format: C
diff --git a/tests/regression/36-apron/52-queuesize.t b/tests/regression/36-apron/52-queuesize.t
@@ -53,7 +53,7 @@ Without diff-box:
       column: 3
       function: push
     location_invariant:
-      string: '- ((long long )capacity) >= -2147483647LL'
+      string: 2147483647LL >= (long long )capacity
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -64,7 +64,7 @@ Without diff-box:
       column: 3
       function: push
     location_invariant:
-      string: (long long )free >= 0LL
+      string: (long long )used + (long long )free == (long long )capacity
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -75,7 +75,7 @@ Without diff-box:
       column: 3
       function: push
     location_invariant:
-      string: (long long )capacity - (long long )free >= 0LL
+      string: (long long )free >= 0LL
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -86,7 +86,7 @@ Without diff-box:
       column: 3
       function: push
     location_invariant:
-      string: ((long long )free + (long long )used) - (long long )capacity == 0LL
+      string: (long long )capacity >= (long long )free
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -97,7 +97,7 @@ Without diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: '- ((long long )capacity) >= -2147483647LL'
+      string: 2147483647LL >= (long long )capacity
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -108,7 +108,7 @@ Without diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: (long long )free >= 0LL
+      string: (long long )used + (long long )free == (long long )capacity
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -119,7 +119,7 @@ Without diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: (long long )capacity - (long long )free >= 0LL
+      string: (long long )free >= 0LL
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -130,7 +130,7 @@ Without diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: ((long long )free + (long long )used) - (long long )capacity == 0LL
+      string: (long long )capacity >= (long long )free
       type: assertion
       format: C
 
@@ -187,7 +187,7 @@ With diff-box:
       column: 3
       function: push
     location_invariant:
-      string: (long long )free >= 0LL
+      string: (long long )used + (long long )free == (long long )capacity
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -198,7 +198,7 @@ With diff-box:
       column: 3
       function: push
     location_invariant:
-      string: (long long )capacity - (long long )free >= 0LL
+      string: (long long )free >= 0LL
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -209,7 +209,7 @@ With diff-box:
       column: 3
       function: push
     location_invariant:
-      string: ((long long )free + (long long )used) - (long long )capacity == 0LL
+      string: (long long )capacity >= (long long )free
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -220,7 +220,7 @@ With diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: (long long )free >= 0LL
+      string: (long long )used + (long long )free == (long long )capacity
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -231,7 +231,7 @@ With diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: (long long )capacity - (long long )free >= 0LL
+      string: (long long )free >= 0LL
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -242,7 +242,7 @@ With diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: ((long long )free + (long long )used) - (long long )capacity == 0LL
+      string: (long long )capacity >= (long long )free
       type: assertion
       format: C
 
@@ -258,7 +258,7 @@ Compare witnesses:
       column: 3
       function: push
     location_invariant:
-      string: '- ((long long )capacity) >= -2147483647LL'
+      string: 2147483647LL >= (long long )capacity
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -269,7 +269,7 @@ Compare witnesses:
       column: 3
       function: pop
     location_invariant:
-      string: '- ((long long )capacity) >= -2147483647LL'
+      string: 2147483647LL >= (long long )capacity
       type: assertion
       format: C
   ---