Merge pull request #1873 from goblint/apron-invariant-diff-box-direct

Implement `ana.apron.invariant.diff-box` directly in domain

Author: sim642

src/analyses/apron/apronAnalysis.apron.ml

@@ -8,8 +8,6 @@ let spec_module: (module MCPSpec) Lazy.t =
   lazy (
     let module Man = (val ApronDomain.get_manager ()) in
     let module AD = ApronDomain.D2 (Man) in
-    let diff_box = GobConfig.get_bool "ana.apron.invariant.diff-box" in
-    let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): RelationDomain.RD) else (module AD)) in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct

src/cdomains/apron/apronDomain.apron.ml

@@ -544,17 +544,37 @@ struct
           d
       end
 
-  let invariant x =
+  (** Keep only box-representable constraints.
+      Used for [diff-box] in {!invariant}. *)
+  let boxify d =
+    let {box1_env; interval_array}: A.box1 = A.to_box Man.mgr d in
+    let ivs, fvs = Environment.vars box1_env in
+    assert (Array.length fvs = 0); (* shouldn't ever contain floats *)
+    A.of_box Man.mgr box1_env ivs interval_array
+
+  let to_lincons_set d =
+    Lincons1Set.of_earray (A.to_lincons_array Man.mgr d)
+
+  let invariant d =
     (* Would like to minimize to get rid of multi-var constraints directly derived from one-var constraints,
        but not implemented in Apron at all: https://github.com/antoinemine/apron/issues/44 *)
-    (* let x = A.copy Man.mgr x in
-       A.minimize Man.mgr x; *)
-    let {lincons0_array; array_env}: Lincons1.earray = A.to_lincons_array Man.mgr x in
-    Array.to_seq lincons0_array
-    |> Seq.map (fun (lincons0: Lincons0.t) -> Lincons1.{lincons0; env = array_env})
-    |> Lincons1Set.of_seq
+    (* let d = A.copy Man.mgr d in
+       A.minimize Man.mgr d; *)
+    let lcd = to_lincons_set d in
+    if GobConfig.get_bool "ana.apron.invariant.diff-box" then (
+      (* diff via lincons *)
+      (* TODO: is there benefit to also Lincons1Set.simplify before diff? might make a difference if y=0 is represented as y>=0 && y<=0 or not *)
+      let b = boxify d in (* convert back to same Apron domain (instead of box) to make lincons use the same format (e.g. oct doesn't return equalities, but box does) *)
+      let lcb = to_lincons_set b in
+      Lincons1Set.diff lcd lcb
+    )
+    else
+      lcd
+
+  let invariant d =
+    invariant d
     |> (if Oct.manager_is_oct Man.mgr then Lincons1Set.simplify else Fun.id)
-    |> Lincons1Set.elements
+    |> Lincons1Set.elements (* TODO: remove list conversion? *)
 end
 
 (** With heterogeneous environments. *)
@@ -836,111 +856,3 @@ struct
 
   let unmarshal (m: marshal) = Oct.Abstract1.of_oct @@ OctagonD.unmarshal m
 end
-
-(** Lift [D] to a non-reduced product with box.
-    Both are updated in parallel, but [D] answers to queries.
-    Box domain is used to filter out non-relational invariants for output. *)
-module BoxProd0 (D: S3) =
-struct
-  module BoxD = D2 (IntervalManager)
-
-  include Printable.Prod (BoxD) (D)
-
-  let equal (_, d1) (_, d2) = D.equal d1 d2
-  let hash (_, d) = D.hash d
-  let compare (_, d1) (_, d2) = D.compare d1 d2
-
-  let leq (_, d1) (_, d2) = D.leq d1 d2
-  let join (b1, d1) (b2, d2) = (BoxD.join b1 b2, D.join d1 d2)
-  let meet (b1, d1) (b2, d2) = (BoxD.meet b1 b2, D.meet d1 d2)
-  let widen (b1, d1) (b2, d2) = (BoxD.widen b1 b2, D.widen d1 d2)
-  let narrow (b1, d1) (b2, d2) = (BoxD.narrow b1 b2, D.narrow d1 d2)
-
-  let top () = (BoxD.top (), D.top ())
-  let bot () = (BoxD.bot (), D.bot ())
-  let is_top (_, d) = D.is_top d
-  let is_bot (_, d) = D.is_bot d
-  let top_env env = (BoxD.top_env env, D.top_env env)
-  let bot_env env = (BoxD.bot_env env, D.bot_env env)
-  let is_top_env (_, d) = D.is_top_env d
-  let is_bot_env (_, d) = D.is_bot_env d
-  let unify (b1, d1) (b2, d2) = (BoxD.unify b1 b2, D.unify d1 d2)
-  let copy (b, d) = (BoxD.copy b, D.copy d)
-
-  type marshal = BoxD.marshal * D.marshal
-
-  let marshal (b, d) = (BoxD.marshal b, D.marshal d)
-  let unmarshal (b, d) = (BoxD.unmarshal b, D.unmarshal d)
-
-  let mem_var (_, d) v = D.mem_var d v
-  let vars (_, d) = D.vars d
-
-  let pretty_diff () ((_, d1), (_, d2)) = D.pretty_diff () (d1, d2)
-
-  let add_vars_with (b, d) vs =
-    BoxD.add_vars_with b vs;
-    D.add_vars_with d vs
-  let remove_vars_with (b, d) vs =
-    BoxD.remove_vars_with b vs;
-    D.remove_vars_with d vs
-  let remove_filter_with (b, d) f =
-    BoxD.remove_filter_with b f;
-    D.remove_filter_with d f
-  let keep_filter_with (b, d) f =
-    BoxD.keep_filter_with b f;
-    D.keep_filter_with d f
-  let keep_vars_with (b, d) vs =
-    BoxD.keep_vars_with b vs;
-    D.keep_vars_with d vs
-  let forget_vars_with (b, d) vs =
-    BoxD.forget_vars_with b vs;
-    D.forget_vars_with d vs
-  let assign_exp_with ask (b, d) v e no_ov =
-    BoxD.assign_exp_with ask b v e no_ov;
-    D.assign_exp_with ask d v e no_ov
-  let assign_exp_parallel_with ask (b, d) ves no_ov =
-    BoxD.assign_exp_parallel_with ask b ves no_ov;
-    D.assign_exp_parallel_with ask d ves no_ov
-  let assign_var_with (b, d) v e =
-    BoxD.assign_var_with b v e;
-    D.assign_var_with d v e
-  let assign_var_parallel_with (b, d) vvs =
-    BoxD.assign_var_parallel_with b vvs;
-    D.assign_var_parallel_with d vvs
-  let assign_var_parallel' (b, d) vs v's =
-    (BoxD.assign_var_parallel' b vs v's, D.assign_var_parallel' d vs v's)
-  let substitute_exp_with ask (b, d) v e no_ov =
-    BoxD.substitute_exp_with ask b v e no_ov;
-    D.substitute_exp_with ask d v e no_ov
-  let substitute_exp_parallel_with ask (b, d) ves no_ov =
-    BoxD.substitute_exp_parallel_with ask b ves no_ov;
-    D.substitute_exp_parallel_with ask d ves no_ov
-  let substitute_var_with (b, d) v1 v2 =
-    BoxD.substitute_var_with b v1 v2;
-    D.substitute_var_with d v1 v2
-  let meet_tcons ask (b, d) c e = (BoxD.meet_tcons ask b c e, D.meet_tcons ask d c e)
-  let to_lincons_array (_, d) = D.to_lincons_array d
-  let of_lincons_array a = (BoxD.of_lincons_array a, D.of_lincons_array a)
-
-  let cil_exp_of_lincons1 = D.cil_exp_of_lincons1
-  let assert_inv ask (b, d) e n no_ov = (BoxD.assert_inv ask b e n no_ov, D.assert_inv ask d e n no_ov)
-  let eval_int ask (_, d) = D.eval_int ask d
-
-  let invariant (b, d) =
-    (* diff via lincons *)
-    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
-
-module BoxProd (D: S3): RD =
-struct
-  module V = D.V
-  type var = V.t
-  module BP0 = BoxProd0 (D)
-  module Tracked = SharedFunctions.Tracked
-  include BP0
-  include AOpsPureOfImperative (BP0)
-end

tests/regression/36-apron/01-octagon_simple.t

@@ -196,7 +196,7 @@ With diff-box:
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (01-octagon_simple.c:44:10-44:11)
   [Info][Witness] witness generation summary:
     location invariants: 0
-    loop invariants: 6
+    loop invariants: 2
     flow-insensitive invariants: 0
     total generation entries: 1
 
@@ -212,24 +212,6 @@ With diff-box:
           function: main
         value: (long long )N >= (long long )X
         format: c_expression
-    - invariant:
-        type: loop_invariant
-        location:
-          file_name: 01-octagon_simple.c
-          line: 10
-          column: 3
-          function: main
-        value: 2147483647LL >= (long long )X
-        format: c_expression
-    - invariant:
-        type: loop_invariant
-        location:
-          file_name: 01-octagon_simple.c
-          line: 10
-          column: 3
-          function: main
-        value: 4294967294LL >= (long long )X + (long long )N
-        format: c_expression
     - invariant:
         type: loop_invariant
         location:
@@ -239,29 +221,29 @@ With diff-box:
           function: two
         value: (long long )N >= (long long )X
         format: c_expression
-    - invariant:
-        type: loop_invariant
-        location:
-          file_name: 01-octagon_simple.c
-          line: 44
-          column: 3
-          function: two
-        value: 2147483647LL >= (long long )X
-        format: c_expression
-    - invariant:
-        type: loop_invariant
-        location:
-          file_name: 01-octagon_simple.c
-          line: 44
-          column: 3
-          function: two
-        value: 4294967294LL >= (long long )X + (long long )N
-        format: c_expression
 
 Compare witnesses:
 
   $ yamlWitnessStripDiff witness-disable-diff-box.yml witness-enable-diff-box.yml
   # Left-only invariants:
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 01-octagon_simple.c
+        line: 44
+        column: 3
+        function: two
+      value: 4294967294LL >= (long long )X + (long long )N
+      format: c_expression
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 01-octagon_simple.c
+        line: 44
+        column: 3
+        function: two
+      value: 2147483647LL >= (long long )X
+      format: c_expression
   - invariant:
       type: loop_invariant
       location:
@@ -307,6 +289,24 @@ Compare witnesses:
         function: two
       value: (long long )N >= 0LL
       format: c_expression
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 01-octagon_simple.c
+        line: 10
+        column: 3
+        function: main
+      value: 4294967294LL >= (long long )X + (long long )N
+      format: c_expression
+  - invariant:
+      type: loop_invariant
+      location:
+        file_name: 01-octagon_simple.c
+        line: 10
+        column: 3
+        function: main
+      value: 2147483647LL >= (long long )X
+      format: c_expression
   - invariant:
       type: loop_invariant
       location:

tests/regression/36-apron/52-queuesize.t

@@ -160,7 +160,7 @@ With diff-box:
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:56:10-56:11)
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:78:12-78:13)
   [Info][Witness] witness generation summary:
-    location invariants: 6
+    location invariants: 4
     loop invariants: 0
     flow-insensitive invariants: 0
     total generation entries: 1
@@ -170,6 +170,7 @@ With diff-box:
     unsafe: 0
     total memory locations: 3
 
+TODO: Should (long long )free >= 0LL somehow still remain, because it cannot be inferred by box alone?
   $ yamlWitnessStrip < witness.yml | tee witness-enable-diff-box.yml
   - entry_type: invariant_set
     content:
@@ -182,15 +183,6 @@ With diff-box:
           function: pop
         value: (long long )capacity >= (long long )free
         format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 52-queuesize.c
-          line: 15
-          column: 3
-          function: pop
-        value: (long long )free >= 0LL
-        format: c_expression
     - invariant:
         type: location_invariant
         location:
@@ -209,15 +201,6 @@ With diff-box:
           function: push
         value: (long long )capacity >= (long long )free
         format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 52-queuesize.c
-          line: 36
-          column: 3
-          function: push
-        value: (long long )free >= 0LL
-        format: c_expression
     - invariant:
         type: location_invariant
         location:
@@ -241,6 +224,15 @@ Compare witnesses:
         function: push
       value: 2147483647LL >= (long long )capacity
       format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 52-queuesize.c
+        line: 36
+        column: 3
+        function: push
+      value: (long long )free >= 0LL
+      format: c_expression
   - invariant:
       type: location_invariant
       location:
@@ -250,4 +242,13 @@ Compare witnesses:
         function: pop
       value: 2147483647LL >= (long long )capacity
       format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 52-queuesize.c
+        line: 15
+        column: 3
+        function: pop
+      value: (long long )free >= 0LL
+      format: c_expression
   ---