Merge branch 'master' into apron_track_address

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
+    }
   }
 }

make.sh

@@ -109,7 +109,7 @@ rule() {
       cp g2html/g2html.jar .
     ;; setup_gobview )
       [[ -f gobview/gobview.opam ]] || git submodule update --init gobview
-      opam install --deps-only --locked gobview/gobview.opam
+      opam install --deps-only --locked gobview/
     # ;; watch)
     #   fswatch --event Updated -e $TARGET.ml src/ | xargs -n1 -I{} make
     ;; install)

scripts/update_suite.rb

@@ -156,8 +156,12 @@ def collect_warnings
                     when /Assertion .* will fail/    then "fail"
                     when /Assertion .* will succeed/ then "success"
                     when /Assertion .* is unknown/   then "unknown"
+                    when /invariant confirmed/       then "success"
+                    when /invariant unconfirmed/     then "unknown"
+                    when /invariant refuted/         then "fail"
                     when /^\[Warning\]/              then "warn"
                     when /^\[Error\]/                then "warn"
+                    when /^\[Success\]/              then "success"
                     when /\[Debug\]/                 then next # debug "warnings" shouldn't count as other warnings (against NOWARN)
                     when /^  on line \d+ $/          then next # dead line warnings shouldn't count (used for unreachability with NOWARN)
                     when /^  on lines \d+..\d+ $/    then next # dead line warnings shouldn't count (used for unreachability with NOWARN)
@@ -192,7 +196,7 @@ def compare_warnings
         check.call warnings[idx] == type
       when "nowarn"
         check.call warnings[idx].nil?
-      when "assert"
+      when "assert", "success"
         check.call warnings[idx] == "success"
       when "norace"
         check.call warnings[idx] != "race"
@@ -285,6 +289,12 @@ def parse_tests (lines)
         tests[i] = if obj =~ /NODEADLOCK/ then "nodeadlock" else "deadlock" end
       elsif obj =~ /WARN/ then
         tests[i] = if obj =~ /NOWARN/ then "nowarn" else "warn" end
+      elsif obj =~ /SUCCESS/ then
+        tests[i] = "success"
+      elsif obj =~ /FAIL/ then
+        tests[i] = "fail"
+      elsif obj =~ /UNKNOWN/ then
+        tests[i] = "unknown"
       elsif obj =~ /assert.*\(/ then
         if obj =~ /FAIL/ then
           tests[i] = "fail"

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
@@ -334,7 +340,7 @@ struct
         | _ -> false (* remove everything else (globals, global privs, reachable things from the caller) *)
       )
     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 (
@@ -443,6 +449,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
@@ -472,6 +506,8 @@ struct
       let exp = (BinOp (Cil.Lt, exp1, exp2, TInt (IInt, []))) in
       let is_lt = eval_int exp in
       Option.default true (ID.to_bool is_lt)
+    | Queries.Invariant context ->
+      query_invariant ctx context
     | _ -> Result.top q
 
 
@@ -523,8 +559,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])
@@ -535,21 +582,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
 
@@ -566,7 +606,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
@@ -47,7 +47,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
@@ -139,7 +139,7 @@ sig
 end
 
 (** Protection-Based Reading. Is unsound w.r.t. to locals escaping and becoming public. *)
-module ProtectionBasedPriv (Param: ProtectionBasedPrivParam): S = functor (AD: ApronDomain.S2) ->
+module ProtectionBasedPriv (Param: ProtectionBasedPrivParam): S = functor (AD: ApronDomain.S3) ->
 struct
   include ConfCheck.RequireMutexActivatedInit
   open Protection
@@ -406,7 +406,7 @@ struct
   let finalize () = ()
 end
 
-module CommonPerMutex = functor(AD: ApronDomain.S2) ->
+module CommonPerMutex = functor(AD: ApronDomain.S3) ->
 struct
   include Protection
   module V = ApronDomain.V
@@ -429,7 +429,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
@@ -572,7 +572,7 @@ struct
 
   let escape node ask getg sideg (st:apron_components_t) escaped : apron_components_t =
     let esc_vars = EscapeDomain.EscapedVars.elements escaped in
-    let esc_vars = List.filter (fun v -> not v.vglob && AD.varinfo_tracked v && AD.mem_var st.apr (AV.local v)) esc_vars in
+    let esc_vars = List.filter (fun v -> not v.vglob && ApronDomain.Tracked.varinfo_tracked v && AD.mem_var st.apr (AV.local v)) esc_vars in
     let escape_one (x:varinfo) st = write_global ask getg sideg st x x in
     List.fold_left (fun st v -> escape_one v st) st esc_vars
 
@@ -590,7 +590,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
 
@@ -604,7 +604,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)
@@ -687,7 +687,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)
@@ -752,7 +752,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)
@@ -828,7 +828,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
@@ -1094,7 +1094,7 @@ struct
 
   let escape node ask getg sideg (st: apron_components_t) escaped: apron_components_t =
     let esc_vars = EscapeDomain.EscapedVars.elements escaped in
-    let esc_vars = List.filter (fun v -> not v.vglob && AD.varinfo_tracked v && AD.mem_var st.apr (AV.local v)) esc_vars in
+    let esc_vars = List.filter (fun v -> not v.vglob && ApronDomain.Tracked.varinfo_tracked v && AD.mem_var st.apr (AV.local v)) esc_vars in
     let escape_one (x:varinfo) st = write_global ask getg sideg st x x in
     List.fold_left (fun st v -> escape_one v st) st esc_vars
 
@@ -1125,7 +1125,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