From bd758497aaf1f184abf0ec3136dbd1ca3a51c141 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 21 Nov 2024 17:36:08 +0200
Subject: [PATCH 01/12] Split up SharedFunctions.cil_exp_of_linexpr1

---
 src/cdomains/apron/sharedFunctions.apron.ml | 77 ++++++++++++---------
 1 file changed, 44 insertions(+), 33 deletions(-)

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index b9d93bfd99..5450fc6d1e 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -249,41 +249,52 @@ module CilOfApron (V: SV) =
 struct
   exception Unsupported_Linexpr1
 
+  let longlong = TInt(ILongLong,[])
+
+
+  let coeff_to_const ~scalewith consider_flip (c:Coeff.union_5) =
+    match c with
+    | Scalar c ->
+      (match int_of_scalar ?scalewith c with
+      | Some i ->
+        let ci,truncation = truncateCilint ILongLong i in
+        if truncation = NoTruncation then
+          if not consider_flip || Z.compare i Z.zero >= 0 then
+            Const (CInt(i,ILongLong,None)), false
+          else
+            (* attempt to negate if that does not cause an overflow *)
+            let cneg, truncation = truncateCilint ILongLong (Z.neg i) in
+            if truncation = NoTruncation then
+              Const (CInt((Z.neg i),ILongLong,None)), true
+            else
+              Const (CInt(i,ILongLong,None)), false
+        else
+          (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; raise Unsupported_Linexpr1)
+      | None -> raise Unsupported_Linexpr1)
+    | _ -> raise Unsupported_Linexpr1
+
+  let cil_exp_of_linexpr1_term ~scalewith (c: Coeff.t) v =
+    match V.to_cil_varinfo v with
+    | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
+      let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
+      let coeff, flip = coeff_to_const ~scalewith true c in
+      let prod = BinOp(Mult, coeff, var, longlong) in
+      prod, flip
+    | None ->
+      M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v;
+      raise Unsupported_Linexpr1
+    | _ ->
+      M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" Var.pretty v;
+      raise Unsupported_Linexpr1
+
   let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) =
-    let longlong = TInt(ILongLong,[]) in
-    let coeff_to_const consider_flip (c:Coeff.union_5) = match c with
-      | Scalar c ->
-        (match int_of_scalar ?scalewith c with
-         | Some i ->
-           let ci,truncation = truncateCilint ILongLong i in
-           if truncation = NoTruncation then
-             if not consider_flip || Z.compare i Z.zero >= 0 then
-               Const (CInt(i,ILongLong,None)), false
-             else
-               (* attempt to negate if that does not cause an overflow *)
-               let cneg, truncation = truncateCilint ILongLong (Z.neg i) in
-               if truncation = NoTruncation then
-                 Const (CInt((Z.neg i),ILongLong,None)), true
-               else
-                 Const (CInt(i,ILongLong,None)), false
-           else
-             (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; raise Unsupported_Linexpr1)
-         | None -> raise Unsupported_Linexpr1)
-      | _ -> raise Unsupported_Linexpr1
-    in
-    let expr = ref (fst @@ coeff_to_const false (Linexpr1.get_cst linexpr1)) in
+    let expr = ref (fst @@ coeff_to_const ~scalewith false (Linexpr1.get_cst linexpr1)) in
     let append_summand (c:Coeff.union_5) v =
-      match V.to_cil_varinfo v with
-      | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
-        let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
-        let coeff, flip = coeff_to_const true c in
-        let prod = BinOp(Mult, coeff, var, longlong) in
-        if flip then
-          expr := BinOp(MinusA,!expr,prod,longlong)
-        else
-          expr := BinOp(PlusA,!expr,prod,longlong)
-      | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v; raise Unsupported_Linexpr1
-      | _ -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" Var.pretty v; raise Unsupported_Linexpr1
+      let prod, flip = cil_exp_of_linexpr1_term ~scalewith c v in
+      if flip then
+        expr := BinOp(MinusA,!expr,prod,longlong)
+      else
+        expr := BinOp(PlusA,!expr,prod,longlong)
     in
     Linexpr1.iter append_summand linexpr1;
     !expr

From 95971af02fa6e80b823ecfba58689a618b99cff2 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 21 Nov 2024 17:57:05 +0200
Subject: [PATCH 02/12] Avoid excessive 0 constants in relational invariants

---
 src/cdomains/apron/sharedFunctions.apron.ml   | 36 ++++++++++++-------
 .../regression/36-apron/12-traces-min-rpb1.t  |  6 ++--
 tests/regression/36-apron/52-queuesize.t      | 20 +++++------
 3 files changed, 35 insertions(+), 27 deletions(-)

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 5450fc6d1e..d7ee465a20 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -288,16 +288,14 @@ struct
       raise Unsupported_Linexpr1
 
   let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) =
-    let expr = ref (fst @@ coeff_to_const ~scalewith false (Linexpr1.get_cst linexpr1)) in
+    let (const, _) = coeff_to_const ~scalewith false (Coeff.neg (Linexpr1.get_cst linexpr1)) in
+    let terms = ref [] in
     let append_summand (c:Coeff.union_5) v =
-      let prod, flip = cil_exp_of_linexpr1_term ~scalewith c v in
-      if flip then
-        expr := BinOp(MinusA,!expr,prod,longlong)
-      else
-        expr := BinOp(PlusA,!expr,prod,longlong)
+      if not (Coeff.is_zero c) then
+        terms := cil_exp_of_linexpr1_term ~scalewith c v :: !terms
     in
     Linexpr1.iter append_summand linexpr1;
-    !expr
+    !terms, const
 
 
   let lcm_den linexpr1 =
@@ -331,12 +329,26 @@ struct
     try
       let linexpr1 = Lincons1.get_linexpr1 lincons1 in
       let common_denominator = lcm_den linexpr1 in
-      let cilexp = cil_exp_of_linexpr1 ~scalewith:common_denominator linexpr1 in
+      let terms, const = cil_exp_of_linexpr1 ~scalewith:common_denominator linexpr1 in
+      let lhs =
+        List.fold_right (fun (term, flip) acc ->
+            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))
+          ) terms None
+      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, cilexp, zero, TInt(IInt,[])))
-      | SUPEQ -> Some (Cil.constFold false @@ BinOp(Ge, cilexp, zero, TInt(IInt,[])))
-      | SUP -> Some (Cil.constFold false @@ BinOp(Gt, cilexp, zero, TInt(IInt,[])))
-      | DISEQ -> Some (Cil.constFold false @@ BinOp(Ne, cilexp, zero, TInt(IInt,[])))
+      | EQ -> Some (Cil.constFold false @@ BinOp(Eq, lhs, rhs, TInt(IInt,[])))
+      | SUPEQ -> Some (Cil.constFold false @@ BinOp(Ge, lhs, rhs, TInt(IInt,[])))
+      | SUP -> Some (Cil.constFold false @@ BinOp(Gt, lhs, rhs, TInt(IInt,[])))
+      | DISEQ -> Some (Cil.constFold false @@ BinOp(Ne, lhs, rhs, TInt(IInt,[])))
       | EQMOD _ -> None
     with
       Unsupported_Linexpr1 -> None
diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t
index 5060f505d9..d377bba818 100644
--- 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: (0LL - (long long )g) + (long long )h == 0LL
+      string: '- ((long long )g) + (long long )h == 0LL'
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -40,7 +40,7 @@
       column: 3
       function: t_fun
     location_invariant:
-      string: (0LL - (long long )g) + (long long )h == 0LL
+      string: '- ((long long )g) + (long long )h == 0LL'
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -51,6 +51,6 @@
       column: 3
       function: t_fun
     location_invariant:
-      string: (0LL - (long long )g) + (long long )h == 0LL
+      string: '- ((long long )g) + (long long )h == 0LL'
       type: assertion
       format: C
diff --git a/tests/regression/36-apron/52-queuesize.t b/tests/regression/36-apron/52-queuesize.t
index 62851f2ec9..6edde6e878 100644
--- 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: 2147483647LL - (long long )capacity >= 0LL
+      string: '- ((long long )capacity) >= -2147483647LL'
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -86,8 +86,7 @@ Without diff-box:
       column: 3
       function: push
     location_invariant:
-      string: ((0LL - (long long )capacity) + (long long )free) + (long long )used ==
-        0LL
+      string: (- ((long long )capacity) + (long long )free) + (long long )used == 0LL
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -98,7 +97,7 @@ Without diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: 2147483647LL - (long long )capacity >= 0LL
+      string: '- ((long long )capacity) >= -2147483647LL'
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -131,8 +130,7 @@ Without diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: ((0LL - (long long )capacity) + (long long )free) + (long long )used ==
-        0LL
+      string: (- ((long long )capacity) + (long long )free) + (long long )used == 0LL
       type: assertion
       format: C
 
@@ -211,8 +209,7 @@ With diff-box:
       column: 3
       function: push
     location_invariant:
-      string: ((0LL - (long long )capacity) + (long long )free) + (long long )used ==
-        0LL
+      string: (- ((long long )capacity) + (long long )free) + (long long )used == 0LL
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -245,8 +242,7 @@ With diff-box:
       column: 3
       function: pop
     location_invariant:
-      string: ((0LL - (long long )capacity) + (long long )free) + (long long )used ==
-        0LL
+      string: (- ((long long )capacity) + (long long )free) + (long long )used == 0LL
       type: assertion
       format: C
 
@@ -262,7 +258,7 @@ Compare witnesses:
       column: 3
       function: push
     location_invariant:
-      string: 2147483647LL - (long long )capacity >= 0LL
+      string: '- ((long long )capacity) >= -2147483647LL'
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -273,7 +269,7 @@ Compare witnesses:
       column: 3
       function: pop
     location_invariant:
-      string: 2147483647LL - (long long )capacity >= 0LL
+      string: '- ((long long )capacity) >= -2147483647LL'
       type: assertion
       format: C
   ---

From cdb4322de57ac5530a41755a78de6b4845b69c91 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 29 Nov 2024 17:43:15 +0200
Subject: [PATCH 03/12] Sort relational invariants to have positive terms first

---
 src/cdomains/apron/sharedFunctions.apron.ml    | 7 ++++---
 tests/regression/36-apron/12-traces-min-rpb1.t | 6 +++---
 tests/regression/36-apron/52-queuesize.t       | 8 ++++----
 3 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index d7ee465a20..a2628d9d44 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -279,7 +279,7 @@ struct
       let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
       let coeff, flip = coeff_to_const ~scalewith true c in
       let prod = BinOp(Mult, coeff, var, longlong) in
-      prod, flip
+      flip, prod
     | None ->
       M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v;
       raise Unsupported_Linexpr1
@@ -330,8 +330,9 @@ struct
       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_right (fun (term, flip) acc ->
+        List.fold_left (fun acc (flip, term) ->
             match acc, flip with
             | None, false ->
               Some term
@@ -340,7 +341,7 @@ struct
             | Some exp, _ ->
               let op = if flip then MinusA else PlusA in
               Some (BinOp (op, exp, term, longlong))
-          ) terms None
+          ) None terms
       in
       let lhs = Option.default zero lhs in
       let rhs = const in
diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t
index d377bba818..f087ef8b16 100644
--- 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 )g) + (long long )h == 0LL'
+      string: (long long )h - (long long )g == 0LL
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -40,7 +40,7 @@
       column: 3
       function: t_fun
     location_invariant:
-      string: '- ((long long )g) + (long long )h == 0LL'
+      string: (long long )h - (long long )g == 0LL
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -51,6 +51,6 @@
       column: 3
       function: t_fun
     location_invariant:
-      string: '- ((long long )g) + (long long )h == 0LL'
+      string: (long long )h - (long long )g == 0LL
       type: assertion
       format: C
diff --git a/tests/regression/36-apron/52-queuesize.t b/tests/regression/36-apron/52-queuesize.t
index 6edde6e878..8d0cf7e97a 100644
--- a/tests/regression/36-apron/52-queuesize.t
+++ b/tests/regression/36-apron/52-queuesize.t
@@ -86,7 +86,7 @@ Without diff-box:
       column: 3
       function: push
     location_invariant:
-      string: (- ((long long )capacity) + (long long )free) + (long long )used == 0LL
+      string: ((long long )free + (long long )used) - (long long )capacity == 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 )capacity) + (long long )free) + (long long )used == 0LL
+      string: ((long long )free + (long long )used) - (long long )capacity == 0LL
       type: assertion
       format: C
 
@@ -209,7 +209,7 @@ With diff-box:
       column: 3
       function: push
     location_invariant:
-      string: (- ((long long )capacity) + (long long )free) + (long long )used == 0LL
+      string: ((long long )free + (long long )used) - (long long )capacity == 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 )capacity) + (long long )free) + (long long )used == 0LL
+      string: ((long long )free + (long long )used) - (long long )capacity == 0LL
       type: assertion
       format: C
 

From 44cc07389b5ac1f690a9e4dd259323f231cc9052 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 29 Nov 2024 17:55:01 +0200
Subject: [PATCH 04/12] Avoid subtraction in relational invariants

By moving terms and constant to other side.
---
 src/cdomains/apron/sharedFunctions.apron.ml   | 34 +++++++++++--------
 .../regression/36-apron/12-traces-min-rpb1.t  |  6 ++--
 tests/regression/36-apron/52-queuesize.t      | 32 ++++++++---------
 3 files changed, 38 insertions(+), 34 deletions(-)

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index a2628d9d44..43345e91f6 100644
--- 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
index f087ef8b16..283d5287d8 100644
--- 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
index 8d0cf7e97a..7be516eb1f 100644
--- 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
   ---

From 482ed840e7ea08fc646d40bf6ec9525beeeefc60 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 29 Nov 2024 18:02:15 +0200
Subject: [PATCH 05/12] Remove unnecessary negation from relational invariant
 generation

---
 src/cdomains/apron/sharedFunctions.apron.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 43345e91f6..2a00c89214 100644
--- 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 true (Coeff.neg (Linexpr1.get_cst linexpr1)) in
+    let const = coeff_to_const ~scalewith true (Linexpr1.get_cst linexpr1) in
     let terms = ref [] in
     let append_summand (c:Coeff.union_5) v =
       if not (Coeff.is_zero c) then
@@ -345,9 +345,9 @@ struct
       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)
+        else
+          BinOp (PlusA, lhs, const, longlong), rhs
       in
       match Lincons1.get_typ lincons1 with
       | EQ -> Some (Cil.constFold false @@ BinOp(Eq, lhs, rhs, TInt(IInt,[])))

From 21872bb379fa4eb21c2087129ed96341190aa85a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 2 Dec 2024 04:23:48 +0200
Subject: [PATCH 06/12] Simplify dual Apron inequalities to one equality

---
 src/cdomains/apron/apronDomain.apron.ml       | 31 ++++++++++++++++++-
 .../regression/36-apron/12-traces-min-rpb1.t  |  3 +-
 2 files changed, 31 insertions(+), 3 deletions(-)

diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 043b728799..4000a6b7ce 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -486,6 +486,32 @@ sig
   val invariant: t -> Lincons1.t list
 end
 
+(* TODO: move these somewhere better *)
+let flip_lincons1 (lincons1: Lincons1.t): Lincons1.t =
+  let r = Lincons1.copy lincons1 in
+  let linexpr0 = r.lincons0.linexpr0 in
+  let n = Linexpr0.get_size linexpr0 in
+  for i = 0 to n - 1 do
+    Linexpr0.set_coeff linexpr0 i (Coeff.neg (Linexpr0.get_coeff linexpr0 i))
+  done;
+  Lincons1.set_cst r (Coeff.neg (Lincons1.get_cst r));
+  r
+
+let simplify_eqs (lincons1s: Lincons1Set.t): Lincons1Set.t =
+  Lincons1Set.fold (fun lincons1 acc ->
+      let flipped = flip_lincons1 lincons1 in
+      if Lincons1Set.mem flipped lincons1s then (
+        if Lincons1.compare lincons1 flipped < 0 then (
+          Lincons1.set_typ flipped EQ; (* reuse flipped copy for equality *)
+          Lincons1Set.add flipped acc
+        )
+        else
+          acc
+      )
+      else
+        Lincons1Set.add lincons1 acc
+    ) lincons1s Lincons1Set.empty
+
 module DWithOps (Man: Manager) (D: SLattice with type t = Man.mt A.t) =
 struct
   include D
@@ -552,7 +578,9 @@ struct
     |> Enum.map (fun (lincons0: Lincons0.t) ->
         Lincons1.{lincons0; env = array_env}
       )
-    |> List.of_enum
+    |> Lincons1Set.of_enum
+    |> simplify_eqs
+    |> Lincons1Set.elements
 end
 
 (** With heterogeneous environments. *)
@@ -928,6 +956,7 @@ struct
     let lcb = D.to_lincons_array (D.of_lincons_array (BoxD.to_lincons_array b)) in (* convert through D to make lincons use the same format *)
     let lcd = D.to_lincons_array d in
     Lincons1Set.(diff (of_earray lcd) (of_earray lcb))
+    |> simplify_eqs
     |> Lincons1Set.elements
 end
 
diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t
index 0111b6da1b..3f2446710c 100644
--- a/tests/regression/36-apron/12-traces-min-rpb1.t
+++ b/tests/regression/36-apron/12-traces-min-rpb1.t
@@ -173,7 +173,6 @@
           format: c_expression
   - entry_type: flow_insensitive_invariant
     flow_insensitive_invariant:
-      string: '! multithreaded || (A_locked || ((long long )g >= (long long )h && (long
-        long )h >= (long long )g))'
+      string: '! multithreaded || (A_locked || (long long )g == (long long )h)'
       type: assertion
       format: C

From 1de9009d750baa69e81ea00deeb5d2e908fbcc54 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 4 Dec 2024 15:05:40 +0200
Subject: [PATCH 07/12] Move Lincons1Set simplification to GobApron

---
 src/cdomains/apron/apronDomain.apron.ml | 30 ++---------------
 src/cdomains/apron/gobApron.apron.ml    | 44 +++++++++++++++++++++++++
 2 files changed, 46 insertions(+), 28 deletions(-)

diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 4000a6b7ce..240683bac7 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -486,32 +486,6 @@ sig
   val invariant: t -> Lincons1.t list
 end
 
-(* TODO: move these somewhere better *)
-let flip_lincons1 (lincons1: Lincons1.t): Lincons1.t =
-  let r = Lincons1.copy lincons1 in
-  let linexpr0 = r.lincons0.linexpr0 in
-  let n = Linexpr0.get_size linexpr0 in
-  for i = 0 to n - 1 do
-    Linexpr0.set_coeff linexpr0 i (Coeff.neg (Linexpr0.get_coeff linexpr0 i))
-  done;
-  Lincons1.set_cst r (Coeff.neg (Lincons1.get_cst r));
-  r
-
-let simplify_eqs (lincons1s: Lincons1Set.t): Lincons1Set.t =
-  Lincons1Set.fold (fun lincons1 acc ->
-      let flipped = flip_lincons1 lincons1 in
-      if Lincons1Set.mem flipped lincons1s then (
-        if Lincons1.compare lincons1 flipped < 0 then (
-          Lincons1.set_typ flipped EQ; (* reuse flipped copy for equality *)
-          Lincons1Set.add flipped acc
-        )
-        else
-          acc
-      )
-      else
-        Lincons1Set.add lincons1 acc
-    ) lincons1s Lincons1Set.empty
-
 module DWithOps (Man: Manager) (D: SLattice with type t = Man.mt A.t) =
 struct
   include D
@@ -579,7 +553,7 @@ struct
         Lincons1.{lincons0; env = array_env}
       )
     |> Lincons1Set.of_enum
-    |> simplify_eqs
+    |> Lincons1Set.simplify
     |> Lincons1Set.elements
 end
 
@@ -956,7 +930,7 @@ struct
     let lcb = D.to_lincons_array (D.of_lincons_array (BoxD.to_lincons_array b)) in (* convert through D to make lincons use the same format *)
     let lcd = D.to_lincons_array d in
     Lincons1Set.(diff (of_earray lcd) (of_earray lcb))
-    |> simplify_eqs
+    |> Lincons1Set.simplify
     |> Lincons1Set.elements
 end
 
diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml
index 327e43e321..890c4af155 100644
--- a/src/cdomains/apron/gobApron.apron.ml
+++ b/src/cdomains/apron/gobApron.apron.ml
@@ -38,6 +38,28 @@ struct
   let equal x y = Var.compare x y = 0
 end
 
+module Linexpr0 =
+struct
+  include Linexpr0
+
+  let neg (linexpr0: t): t =
+    let r = copy linexpr0 in
+    let n = Linexpr0.get_size r in
+    for i = 0 to n - 1 do
+      Linexpr0.set_coeff r i (Coeff.neg (Linexpr0.get_coeff r i))
+    done;
+    Linexpr0.set_cst r (Coeff.neg (Linexpr0.get_cst r));
+    r
+end
+
+module Linexpr1 =
+struct
+  include Linexpr1
+
+  let neg (linexpr1: t): t =
+    {linexpr0 = Linexpr0.neg linexpr1.linexpr0; env = linexpr1.env}
+end
+
 module Lincons1 =
 struct
   include Lincons1
@@ -62,6 +84,9 @@ struct
           incr size
       ) x;
     !size
+
+  let flip (lincons1: t): t =
+    make (Linexpr1.neg (get_linexpr1 lincons1)) (get_typ lincons1)
 end
 
 module Lincons1Set =
@@ -74,6 +99,25 @@ struct
         Lincons1.{lincons0; env = array_env}
       )
     |> of_enum
+
+  let simplify (lincons1s: t): t =
+    fold (fun lincons1 acc ->
+        match Lincons1.get_typ lincons1 with
+        | SUPEQ ->
+          let flipped = Lincons1.flip lincons1 in
+          if mem flipped lincons1s then (
+            if Lincons1.compare lincons1 flipped < 0 then (
+              Lincons1.set_typ flipped EQ; (* reuse flipped copy for equality *)
+              add flipped acc
+            )
+            else
+              acc
+          )
+          else
+            add lincons1 acc
+        | _ ->
+          add lincons1 acc
+      ) lincons1s empty
 end
 
 module Texpr1 =

From dc7a84969a0853b4b3d8beeaeaf21424c65bc8c6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 4 Dec 2024 15:10:52 +0200
Subject: [PATCH 08/12] Remove always true consider_flip argument from Apron
 coeff_to_const

---
 src/cdomains/apron/sharedFunctions.apron.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 2a00c89214..f5d7d8b7bd 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -252,14 +252,14 @@ struct
   let longlong = TInt(ILongLong,[])
 
 
-  let coeff_to_const ~scalewith consider_flip (c:Coeff.union_5) =
+  let coeff_to_const ~scalewith (c:Coeff.union_5) =
     match c with
     | Scalar c ->
       (match int_of_scalar ?scalewith c with
       | Some i ->
         let ci,truncation = truncateCilint ILongLong i in
         if truncation = NoTruncation then
-          if not consider_flip || Z.compare i Z.zero >= 0 then
+          if Z.compare i Z.zero >= 0 then
             Const (CInt(i,ILongLong,None)), false
           else
             (* attempt to negate if that does not cause an overflow *)
@@ -277,7 +277,7 @@ struct
     match V.to_cil_varinfo v with
     | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
       let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
-      let coeff, flip = coeff_to_const ~scalewith true c in
+      let coeff, flip = coeff_to_const ~scalewith c in
       let prod = BinOp(Mult, coeff, var, longlong) in
       flip, prod
     | None ->
@@ -288,7 +288,7 @@ struct
       raise Unsupported_Linexpr1
 
   let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) =
-    let const = coeff_to_const ~scalewith true (Linexpr1.get_cst linexpr1) in
+    let const = coeff_to_const ~scalewith (Linexpr1.get_cst linexpr1) in
     let terms = ref [] in
     let append_summand (c:Coeff.union_5) v =
       if not (Coeff.is_zero c) then

From c69622ded8bf77c145b8a15f81886b56bc0967a2 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 4 Dec 2024 15:25:07 +0200
Subject: [PATCH 09/12] Refactor Apron cil_exp_of_lincons1

---
 src/cdomains/apron/sharedFunctions.apron.ml | 38 +++++++++------------
 1 file changed, 16 insertions(+), 22 deletions(-)

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index f5d7d8b7bd..1ade3195ef 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -260,14 +260,14 @@ struct
         let ci,truncation = truncateCilint ILongLong i in
         if truncation = NoTruncation then
           if Z.compare i Z.zero >= 0 then
-            Const (CInt(i,ILongLong,None)), false
+            false, Const (CInt(i,ILongLong,None))
           else
             (* attempt to negate if that does not cause an overflow *)
             let cneg, truncation = truncateCilint ILongLong (Z.neg i) in
             if truncation = NoTruncation then
-              Const (CInt((Z.neg i),ILongLong,None)), true
+              true, Const (CInt((Z.neg i),ILongLong,None))
             else
-              Const (CInt(i,ILongLong,None)), false
+              false, Const (CInt(i,ILongLong,None))
         else
           (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; raise Unsupported_Linexpr1)
       | None -> raise Unsupported_Linexpr1)
@@ -277,7 +277,7 @@ struct
     match V.to_cil_varinfo v with
     | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
       let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
-      let coeff, flip = coeff_to_const ~scalewith c in
+      let flip, coeff = coeff_to_const ~scalewith c in
       let prod = BinOp(Mult, coeff, var, longlong) in
       flip, prod
     | None ->
@@ -288,14 +288,13 @@ struct
       raise Unsupported_Linexpr1
 
   let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) =
-    let const = coeff_to_const ~scalewith (Linexpr1.get_cst linexpr1) in
-    let terms = ref [] in
+    let terms = ref [coeff_to_const ~scalewith (Linexpr1.get_cst linexpr1)] in
     let append_summand (c:Coeff.union_5) v =
       if not (Coeff.is_zero c) then
         terms := cil_exp_of_linexpr1_term ~scalewith c v :: !terms
     in
     Linexpr1.iter append_summand linexpr1;
-    !terms, const
+    !terms
 
 
   let lcm_den linexpr1 =
@@ -329,10 +328,8 @@ struct
     try
       let linexpr1 = Lincons1.get_linexpr1 lincons1 in
       let common_denominator = lcm_den linexpr1 in
-      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 terms = cil_exp_of_linexpr1 ~scalewith:common_denominator linexpr1 in
+      let (nterms, pterms) = Tuple2.mapn (List.map snd) (List.partition fst terms) in
       let fold_terms terms =
         List.fold_left (fun acc term ->
             match acc with
@@ -343,18 +340,15 @@ struct
       in
       let lhs = fold_terms pterms in
       let rhs = fold_terms nterms in
-      let (lhs, rhs) =
-        if constflip then
-          lhs, BinOp (PlusA, rhs, const, longlong)
-        else
-          BinOp (PlusA, lhs, const, longlong), rhs
+      let binop =
+        match Lincons1.get_typ lincons1 with
+        | EQ -> Eq
+        | SUPEQ -> Ge
+        | SUP -> Gt
+        | DISEQ -> Ne
+        | EQMOD _ -> raise Unsupported_Linexpr1
       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,[])))
-      | SUP -> Some (Cil.constFold false @@ BinOp(Gt, lhs, rhs, TInt(IInt,[])))
-      | DISEQ -> Some (Cil.constFold false @@ BinOp(Ne, lhs, rhs, TInt(IInt,[])))
-      | EQMOD _ -> None
+      Some (Cil.constFold false @@ BinOp(binop, lhs, rhs, TInt(IInt,[])))
     with
       Unsupported_Linexpr1 -> None
 end

From 819c06129de4d168d399af63a3de9c70dc4ea3ca Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 14 Jan 2025 12:46:31 +0200
Subject: [PATCH 10/12] Remove fixed TODOs about octagon exact invariant
 filtering

---
 src/analyses/apron/relationAnalysis.apron.ml | 2 +-
 src/analyses/apron/relationPriv.apron.ml     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index df3cf545c5..95ce0fe20b 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -624,7 +624,7 @@ struct
     |> List.enum
     |> Enum.filter_map (fun (lincons1: Apron.Lincons1.t) ->
         (* filter one-vars and exact *)
-        (* TODO: exact filtering doesn't really work with octagon because it returns two SUPEQ constraints instead *)
+        (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *)
         if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
           RD.cil_exp_of_lincons1 lincons1
           |> Option.map e_inv
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 257bec24d8..65d6941530 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -728,7 +728,7 @@ struct
           |> List.enum
           |> Enum.filter_map (fun (lincons1: Apron.Lincons1.t) ->
               (* filter one-vars and exact *)
-              (* TODO: exact filtering doesn't really work with octagon because it returns two SUPEQ constraints instead *)
+              (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *)
               if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
                 RD.cil_exp_of_lincons1 lincons1
                 |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp))

From 78d8bceeb92fd7dec2ba186386034c98434b7e12 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 14 Jan 2025 12:54:33 +0200
Subject: [PATCH 11/12] Restrict invariant simplification to octagon domain

Other Apron domans output equalities.
---
 src/cdomains/apron/apronDomain.apron.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 240683bac7..751db12dba 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -553,7 +553,7 @@ struct
         Lincons1.{lincons0; env = array_env}
       )
     |> Lincons1Set.of_enum
-    |> Lincons1Set.simplify
+    |> (if Oct.manager_is_oct Man.mgr then Lincons1Set.simplify else Fun.id)
     |> Lincons1Set.elements
 end
 
@@ -810,6 +810,7 @@ sig
 
   module V: RV
   module Tracked: RelationDomain.Tracked
+  module Man: Manager
 
   val assert_inv : Queries.ask -> t -> exp -> bool -> bool Lazy.t -> t
   val eval_int : Queries.ask -> t -> exp -> bool Lazy.t -> Queries.ID.t
@@ -930,7 +931,7 @@ struct
     let lcb = D.to_lincons_array (D.of_lincons_array (BoxD.to_lincons_array b)) in (* convert through D to make lincons use the same format *)
     let lcd = D.to_lincons_array d in
     Lincons1Set.(diff (of_earray lcd) (of_earray lcb))
-    |> Lincons1Set.simplify
+    |> (if Oct.manager_is_oct D.Man.mgr then Lincons1Set.simplify else Fun.id)
     |> Lincons1Set.elements
 end
 

From b2a98c3965b5c1d2e56cb18d6a3caeb5582a3b26 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 14 Jan 2025 13:04:37 +0200
Subject: [PATCH 12/12] Document new GobApron functions

---
 src/cdomains/apron/gobApron.apron.ml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml
index 890c4af155..6a995e69de 100644
--- a/src/cdomains/apron/gobApron.apron.ml
+++ b/src/cdomains/apron/gobApron.apron.ml
@@ -42,6 +42,7 @@ module Linexpr0 =
 struct
   include Linexpr0
 
+  (** Negate linear expression. *)
   let neg (linexpr0: t): t =
     let r = copy linexpr0 in
     let n = Linexpr0.get_size r in
@@ -56,6 +57,7 @@ module Linexpr1 =
 struct
   include Linexpr1
 
+  (** Negate linear expression. *)
   let neg (linexpr1: t): t =
     {linexpr0 = Linexpr0.neg linexpr1.linexpr0; env = linexpr1.env}
 end
@@ -85,7 +87,10 @@ struct
       ) x;
     !size
 
+  (** Flip comparison operator in linear constraint, i.e., swap sides. *)
   let flip (lincons1: t): t =
+    (* Apron constraints have rhs 0 and inequality only in one direction, so do the following: *)
+    (* e >= 0  ->  e <= 0  ->  -e >= 0 *)
     make (Linexpr1.neg (get_linexpr1 lincons1)) (get_typ lincons1)
 end
 
@@ -100,6 +105,7 @@ struct
       )
     |> of_enum
 
+  (** Simplify (octagon) constraint set to replace two {!SUPEQ}-s with single {!EQ}. *)
   let simplify (lincons1s: t): t =
     fold (fun lincons1 acc ->
         match Lincons1.get_typ lincons1 with