Merge pull request #1630 from goblint/apron-invariant-simplify

Simplify relational witness invariants

Author: sim642

src/analyses/apron/relationAnalysis.apron.ml

@@ -619,7 +619,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

src/analyses/apron/relationPriv.apron.ml

@@ -730,7 +730,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))

src/cdomains/apron/apronDomain.apron.ml

@@ -552,7 +552,9 @@ struct
     |> Enum.map (fun (lincons0: Lincons0.t) ->
         Lincons1.{lincons0; env = array_env}
       )
-    |> List.of_enum
+    |> Lincons1Set.of_enum
+    |> (if Oct.manager_is_oct Man.mgr then Lincons1Set.simplify else Fun.id)
+    |> Lincons1Set.elements
 end
 
 (** With heterogeneous environments. *)
@@ -808,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
@@ -928,6 +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))
+    |> (if Oct.manager_is_oct D.Man.mgr then Lincons1Set.simplify else Fun.id)
     |> Lincons1Set.elements
 end
 

src/cdomains/apron/gobApron.apron.ml

@@ -38,6 +38,30 @@ struct
   let equal x y = Var.compare x y = 0
 end
 
+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
+    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
+
+  (** Negate linear expression. *)
+  let neg (linexpr1: t): t =
+    {linexpr0 = Linexpr0.neg linexpr1.linexpr0; env = linexpr1.env}
+end
+
 module Lincons1 =
 struct
   include Lincons1
@@ -62,6 +86,12 @@ struct
           incr size
       ) 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
 
 module Lincons1Set =
@@ -74,6 +104,26 @@ struct
         Lincons1.{lincons0; env = array_env}
       )
     |> 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
+        | 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 =

src/cdomains/apron/sharedFunctions.apron.ml

@@ -268,44 +268,55 @@ module CilOfApron (V: SV) =
 struct
   exception Unsupported_Linexpr1
 
+  let longlong = TInt(ILongLong,[])
+
+
+  (** Returned boolean indicates whether returned expression should be negated. *)
+  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 Z.compare i Z.zero >= 0 then
+            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
+              true, Const (CInt((Z.neg i),ILongLong,None))
+            else
+              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)
+    | _ -> raise Unsupported_Linexpr1
+
+  (** Returned boolean indicates whether returned expression should be negated. *)
+  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 flip, coeff = coeff_to_const ~scalewith c in
+      let prod = BinOp(Mult, coeff, var, longlong) in
+      flip, prod
+    | 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
+
+  (** Returned booleans indicates whether returned expressions should be negated. *)
   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 terms = ref [coeff_to_const ~scalewith (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
+      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
 
 
   let lcm_den linexpr1 =
@@ -339,13 +350,27 @@ 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
-      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,[])))
-      | EQMOD _ -> None
+      let terms = cil_exp_of_linexpr1 ~scalewith:common_denominator linexpr1 in
+      let (nterms, pterms) = Tuple2.mapn (List.map snd) (List.partition fst terms) in (* partition terms into negative (nterms) and positive (pterms) *)
+      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 (* negative terms are moved from Apron's lhs to our rhs, so they all become positive there *)
+      let binop =
+        match Lincons1.get_typ lincons1 with
+        | EQ -> Eq
+        | SUPEQ -> Ge
+        | SUP -> Gt
+        | DISEQ -> Ne
+        | EQMOD _ -> raise Unsupported_Linexpr1
+      in
+      Some (Cil.constFold false @@ BinOp(binop, lhs, rhs, TInt(IInt,[]))) (* constFold removes multiplication by factor 1 *)
     with
       Unsupported_Linexpr1 -> None
 end

tests/regression/36-apron/12-traces-min-rpb1.t

@@ -31,7 +31,7 @@
       column: 3
       function: main
     location_invariant:
-      string: (0LL - (long long )g) + (long long )h == 0LL
+      string: (long long )h == (long long )g
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -41,7 +41,7 @@
       column: 3
       function: t_fun
     location_invariant:
-      string: (0LL - (long long )g) + (long long )h == 0LL
+      string: (long long )h == (long long )g
       type: assertion
       format: C
   - entry_type: location_invariant
@@ -51,7 +51,7 @@
       column: 3
       function: t_fun
     location_invariant:
-      string: (0LL - (long long )g) + (long long )h == 0LL
+      string: (long long )h == (long long )g
       type: assertion
       format: C
 
@@ -163,7 +163,6 @@
           format: c_expression
   - entry_type: flow_insensitive_invariant
     flow_insensitive_invariant:
-      string: '! multithreaded || (A_locked || ((0LL - (long long )g) + (long long )h
-        >= 0LL && (long long )g - (long long )h >= 0LL))'
+      string: '! multithreaded || (A_locked || (long long )g == (long long )h)'
       type: assertion
       format: C