Merge pull request #762 from goblint/apron-box-prod

Add Apron box product lifter

Author: sim642

conf/traces-rel.json

@@ -26,7 +26,18 @@
       ]
     },
     "base" : {
-      "privatization": "mutex-meet"
+      "privatization": "mutex-meet",
+      "invariant": {
+        "enabled": false
+      }
+    },
+    "apron": {
+      "invariant": {
+        "one-var": false,
+        "local": false,
+        "global": true,
+        "diff-box": true
+      }
     }
   },
   "sem": {
@@ -38,6 +49,9 @@
     },
     "builtin_unreachable": {
       "dead_code": true
+    },
+    "int": {
+      "signed_overflow": "assume_none"
     }
   },
   "exp": {
@@ -52,5 +66,12 @@
     "print_tids" : true,
     "print_wpoints" : true,
     "print_protection": true
+  },
+  "witness": {
+    "invariant": {
+      "other": false,
+      "loop-head": false,
+      "after-lock": true
+    }
   }
 }

src/analyses/apron/apronAnalysis.apron.ml

@@ -6,12 +6,18 @@ open ApronDomain
 
 module M = Messages
 
-module SpecFunctor (AD: ApronDomain.S2) (Priv: ApronPriv.S) : Analyses.MCPSpec =
+module SpecFunctor (AD: ApronDomain.S3) (Priv: ApronPriv.S) : Analyses.MCPSpec =
 struct
   include Analyses.DefaultSpec
 
   let name () = "apron"
 
+  module AD =
+  struct
+    include AD
+    include ApronDomain.Tracked
+  end
+
   module Priv = Priv(AD)
   module D = ApronComponents (AD) (Priv.D)
   module G = Priv.G
@@ -282,7 +288,7 @@ struct
         | _ -> false (* remove everything else (globals, global privs) *)
       )
     in
-    let unify_apr = ApronDomain.A.unify Man.mgr new_apr new_fun_apr in (* TODO: unify_with *)
+    let unify_apr = AD.unify new_apr new_fun_apr in (* TODO: unify_with *)
     if M.tracing then M.tracel "combine" "apron unifying %a %a = %a\n" AD.pretty new_apr AD.pretty new_fun_apr AD.pretty unify_apr;
     let unify_st = {fun_st with apr = unify_apr} in
     if AD.type_tracked (Cilfacade.fundec_return_type f) then (
@@ -354,6 +360,34 @@ struct
       | None -> st'
 
 
+  let query_invariant ctx context =
+    let keep_local = GobConfig.get_bool "ana.apron.invariant.local" in
+    let keep_global = GobConfig.get_bool "ana.apron.invariant.global" in
+
+    let apr = ctx.local.apr in
+    (* filter variables *)
+    let var_filter v = match V.find_metadata v with
+      | Some (Global _) -> keep_global
+      | Some Local -> keep_local
+      | _ -> false
+    in
+    let apr = AD.keep_filter apr var_filter in
+
+    let one_var = GobConfig.get_bool "ana.apron.invariant.one-var" in
+    let scope = Node.find_fundec ctx.node in
+
+    AD.invariant ~scope apr
+    |> List.enum
+    |> Enum.filter_map (fun (lincons1: Lincons1.t) ->
+        (* filter one-vars *)
+        if one_var || Apron.Linexpr0.get_size lincons1.lincons0.linexpr0 >= 2 then
+          CilOfApron.cil_exp_of_lincons1 scope lincons1
+          |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp) && InvariantCil.exp_is_in_scope scope exp)
+        else
+          None
+      )
+    |> Enum.fold (fun acc x -> Invariant.(acc && of_exp x)) Invariant.none
+
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     let open Queries in
     let st = ctx.local in
@@ -383,8 +417,7 @@ struct
       let is_lt = eval_int exp in
       Option.default true (ID.to_bool is_lt)
     | Queries.Invariant context ->
-      let scope = Node.find_fundec ctx.node in
-      D.invariant ~scope ctx.local
+      query_invariant ctx context
     | _ -> Result.top q
 
 
@@ -434,8 +467,19 @@ struct
   let sync ctx reason =
     (* After the solver is finished, store the results (for later comparison) *)
     if !GU.postsolving then begin
+      let keep_local = GobConfig.get_bool "ana.apron.invariant.local" in
+      let keep_global = GobConfig.get_bool "ana.apron.invariant.global" in
+
+      (* filter variables *)
+      let var_filter v = match V.find_metadata v with
+        | Some (Global _) -> keep_global
+        | Some Local -> keep_local
+        | _ -> false
+      in
+      let st = keep_filter ctx.local.apr var_filter in
+
       let old_value = RH.find_default results ctx.node (AD.bot ()) in
-      let new_value = AD.join old_value ctx.local.apr in
+      let new_value = AD.join old_value st in
       RH.replace results ctx.node new_value;
     end;
     Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `Return | `Init | `Thread])
@@ -446,21 +490,14 @@ struct
   module OctApron = ApronPrecCompareUtil.OctagonD
   let store_data file =
     let convert (m: AD.t RH.t): OctApron.t RH.t =
-      let convert_single (a: AD.t): OctApron.t =
-        if Oct.manager_is_oct AD.Man.mgr then
-          Oct.Abstract1.to_oct a
-        else
-          let generator = AD.to_lincons_array a in
-          OctApron.of_lincons_array generator
-      in
-      RH.map (fun _ -> convert_single) m
+      RH.map (fun _ -> AD.to_oct) m
     in
     let post_process m =
       let m = Stats.time "convert" convert m in
       RH.map (fun _ v -> OctApron.marshal v) m
     in
     let results = post_process results in
-    let name = name () ^ "(domain: " ^ (AD.Man.name ()) ^ ", privatization: " ^ (Priv.name ()) ^ (if GobConfig.get_bool "ana.apron.threshold_widening" then ", th" else "" ) ^ ")" in
+    let name = name () ^ "(domain: " ^ (AD.name ()) ^ ", privatization: " ^ (Priv.name ()) ^ (if GobConfig.get_bool "ana.apron.threshold_widening" then ", th" else "" ) ^ ")" in
     let results: ApronPrecCompareUtil.dump = {marshalled = results; name } in
     Serialize.marshal results file
 
@@ -477,7 +514,9 @@ end
 let spec_module: (module MCPSpec) Lazy.t =
   lazy (
     let module Man = (val ApronDomain.get_manager ()) in
-    let module AD = ApronDomain.D2 (Man) in
+    let module AD = ApronDomain.D3 (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): ApronDomain.S3) else (module AD)) in
     let module Priv = (val ApronPriv.get_priv ()) in
     let module Spec = SpecFunctor (AD) (Priv) in
     (module Spec)

src/analyses/apron/apronPriv.apron.ml

@@ -12,7 +12,7 @@ open CommonPriv
 
 
 module type S =
-  functor (AD: ApronDomain.S2) ->
+  functor (AD: ApronDomain.S3) ->
   sig
     module D: Lattice.S
     module G: Lattice.S
@@ -46,7 +46,7 @@ module type S =
 
 (** Top privatization, which doesn't track globals at all.
     This is unlike base's "none" privatization. which does track globals, but doesn't privatize them. *)
-module Top: S = functor (AD: ApronDomain.S2) ->
+module Top: S = functor (AD: ApronDomain.S3) ->
 struct
   module D = Lattice.Unit
   module G = Lattice.Unit
@@ -123,7 +123,7 @@ sig
 end
 
 (** Protection-Based Reading. *)
-module ProtectionBasedPriv (Param: ProtectionBasedPrivParam): S = functor (AD: ApronDomain.S2) ->
+module ProtectionBasedPriv (Param: ProtectionBasedPrivParam): S = functor (AD: ApronDomain.S3) ->
 struct
   include ConfCheck.RequireMutexActivatedInit
   open Protection
@@ -388,7 +388,7 @@ struct
   let finalize () = ()
 end
 
-module CommonPerMutex = functor(AD: ApronDomain.S2) ->
+module CommonPerMutex = functor(AD: ApronDomain.S3) ->
 struct
   include Protection
   module V = ApronDomain.V
@@ -411,7 +411,7 @@ struct
 end
 
 (** Per-mutex meet. *)
-module PerMutexMeetPriv : S = functor (AD: ApronDomain.S2) ->
+module PerMutexMeetPriv : S = functor (AD: ApronDomain.S3) ->
 struct
   open CommonPerMutex(AD)
   include MutexGlobals
@@ -566,7 +566,7 @@ struct
   let name () = "W"
 end
 
-module type ClusterArg = functor (AD: ApronDomain.S2) ->
+module type ClusterArg = functor (AD: ApronDomain.S3) ->
 sig
   module LAD: Lattice.S
 
@@ -580,7 +580,7 @@ sig
 end
 
 (** No clustering. *)
-module NoCluster:ClusterArg = functor (AD: ApronDomain.S2) ->
+module NoCluster:ClusterArg = functor (AD: ApronDomain.S3) ->
 struct
   module AD = AD
   open CommonPerMutex(AD)
@@ -663,7 +663,7 @@ end
 
 
 (** Clusters when clustering is downward-closed. *)
-module DownwardClosedCluster (ClusteringArg: ClusteringArg) =  functor (AD: ApronDomain.S2) ->
+module DownwardClosedCluster (ClusteringArg: ClusteringArg) =  functor (AD: ApronDomain.S3) ->
 struct
   module AD = AD
   open CommonPerMutex(AD)
@@ -728,7 +728,7 @@ struct
 end
 
 (** Clusters when clustering is arbitrary (not necessarily downward-closed). *)
-module ArbitraryCluster (ClusteringArg: ClusteringArg): ClusterArg = functor (AD: ApronDomain.S2) ->
+module ArbitraryCluster (ClusteringArg: ClusteringArg): ClusterArg = functor (AD: ApronDomain.S3) ->
 struct
   module AD = AD
   module DCCluster = (DownwardClosedCluster(ClusteringArg))(AD)
@@ -804,7 +804,7 @@ struct
 end
 
 (** Per-mutex meet with TIDs. *)
-module PerMutexMeetPrivTID (Cluster: ClusterArg): S  = functor (AD: ApronDomain.S2) ->
+module PerMutexMeetPrivTID (Cluster: ClusterArg): S  = functor (AD: ApronDomain.S3) ->
 struct
   open CommonPerMutex(AD)
   include MutexGlobals
@@ -1095,7 +1095,7 @@ struct
   let finalize () = finalize ()
 end
 
-module TracingPriv = functor (Priv: S) -> functor (AD: ApronDomain.S2) ->
+module TracingPriv = functor (Priv: S) -> functor (AD: ApronDomain.S3) ->
 struct
   module Priv = Priv (AD)
   include Priv

src/analyses/base.ml

@@ -1128,6 +1128,12 @@ struct
 
     cpa_invariant
 
+  let query_invariant ctx context =
+    if GobConfig.get_bool "ana.base.invariant.enabled" then
+      query_invariant ctx context
+    else
+      Invariant.none
+
   let query ctx (type a) (q: a Q.t): a Q.result =
     match q with
     | Q.EvalFunvar e ->