Merge branch 'master' into interactive

.gitignore

@@ -58,6 +58,7 @@ goblint.bc.js
 sv-comp/goblint.zip
 
 privPrecCompare*
+apronPrecCompare
 tests/regression/*/run
 
 # csmith

make.sh

@@ -62,6 +62,11 @@ rule() {
       dune build src/privPrecCompare.exe &&
       cp _build/default/src/privPrecCompare.exe privPrecCompare
       chmod +w privPrecCompare
+    ;; apronPrecCompare)
+      eval $(opam config env)
+      dune build src/apronPrecCompare.exe &&
+      cp _build/default/src/apronPrecCompare.exe apronPrecCompare
+      chmod +w apronPrecCompare
     # old rules using ocamlbuild
     ;; ocbnat*)
       ocb -no-plugin $TARGET.native &&

src/analyses/apron/apronAnalysis.apron.ml

@@ -10,6 +10,7 @@ module SpecFunctor (AD: ApronDomain.S2) (Priv: ApronPriv.S) : Analyses.MCPSpec =
 struct
   include Analyses.DefaultSpec
 
+
   let name () = "apron"
 
   module Priv = Priv(AD)
@@ -19,6 +20,10 @@ struct
 
   open AD
 
+  open ApronPrecCompareUtil
+  (* Result map used for comparison of results *)
+  let results = RH.create 103
+
   let should_join = Priv.should_join
 
   let context fd x =
@@ -378,12 +383,40 @@ struct
       st
 
   let sync ctx reason =
+    (* After the solver is finished, store the results (for later comparison) *)
+    if !GU.postsolving then begin
+      let old_value = RH.find_default results ctx.node (AD.bot ()) in
+      let new_value = AD.join old_value ctx.local.apr 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])
 
   let init marshal =
     Priv.init ()
 
+  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 =
+        let generator = AD.to_lincons_array a in
+        OctApron.of_lincons_array generator
+      in
+      RH.map (fun _ -> convert_single) m
+    in
+    let post_process m =
+      let m = 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 ()) ^ ")" in
+    let results: ApronPrecCompareUtil.dump = {marshalled = results; name } in
+    Serialize.marshal results file
+
   let finalize () =
+    let file = GobConfig.get_string "exp.apron.prec-dump" in
+    if file <> "" then begin
+      store_data file
+    end;
     Priv.finalize ()
 end
 

src/analyses/apron/apronPriv.apron.ml

@@ -18,6 +18,7 @@ module type S =
     module G: Lattice.S
 
     type apron_components_t := ApronDomain.ApronComponents (AD) (D).t
+    val name: unit -> string
     val startstate: unit -> D.t
     val should_join: apron_components_t -> apron_components_t -> bool
 
@@ -46,6 +47,7 @@ struct
   module D = Lattice.Unit
   module G = Lattice.Unit
 
+  let name () = "Dummy"
   let startstate () = ()
   let should_join _ _ = true
 
@@ -120,6 +122,8 @@ struct
     let prot g = make_var (Prot g)
   end
 
+  let name () = "ProtectionBasedPriv"
+
   (** Restrict environment to global invariant variables. *)
   let restrict_global apr =
     AD.remove_filter apr (fun var ->
@@ -318,6 +322,8 @@ struct
 
   module V = ApronDomain.V
 
+  let name () = "PerMutexMeetPriv"
+
   let startstate () = ()
 
   let should_join _ _ = true
@@ -480,6 +486,8 @@ struct
   type apron_components_t =  ApronDomain.ApronComponents (AD) (D).t
   let global_varinfo = RichVarinfo.single ~name:"APRON_GLOBAL"
 
+  let name () = "WriteCenteredPriv"
+
   let startstate () = (W.bot (), P.top ())
 
   let should_join _ _ = true

src/analyses/basePriv.ml

@@ -1418,6 +1418,7 @@ struct
   include Priv
 
   open PrivPrecCompareUtil
+  module LVH = RH
 
   let is_dumping = ref false
   let lvh = LVH.create 113
@@ -1438,7 +1439,7 @@ struct
     (* LVH.iter (fun (l, x) v ->
         ignore (Pretty.printf "%a %a = %a\n" CilType.Location.pretty l d_varinfo x VD.pretty v)
       ) lvh; *)
-    Marshal.output f {name = get_string "exp.privatization"; lvh};
+    Marshal.output f ({name = get_string "exp.privatization"; results = lvh}: result);
     close_out_noerr f
 
   let finalize () =

src/analyses/symbLocks.ml

@@ -44,7 +44,7 @@ struct
     List.fold_right D.remove_var (fundec.sformals@fundec.slocals) ctx.local
 
   let enter ctx lval f args = [(ctx.local,ctx.local)]
-  let combine ctx lval fexp f args fc st2 = ctx.local
+  let combine ctx lval fexp f args fc st2 = st2
 
   let get_locks e st =
     let add_perel x xs =

src/apronPrecCompare.ml

@@ -0,0 +1,6 @@
+(* Utility program to compare precision of results of the apron analysis with different privatizations and/or differents apron domains *)
+(* The result files that can be compared here may be created by passing an output file name in "exp.apron.prec-dump" to Goblint *)
+module B = PrecCompare.MakeDump (ApronPrecCompareUtil)
+
+let () =
+  B.main ()

src/cdomains/apron/apronDomain.apron.ml

@@ -28,7 +28,7 @@ sig
   type mt
   type t = mt Apron.Manager.t
   val mgr : mt Apron.Manager.t
-  val name : string
+  val name : unit -> string
 end
 
 (** Manager for the Oct domain, i.e. an octagon domain.
@@ -42,7 +42,7 @@ struct
 
   (* Create the manager *)
   let mgr =  Oct.manager_alloc ()
-  let name = "Octagon manager"
+  let name () = "Octagon"
 end
 
 (** Manager for the Polka domain, i.e. a polyhedra domain.
@@ -54,7 +54,7 @@ struct
   type t = mt Manager.t
   (* Create manager that fits to loose polyhedra *)
   let mgr = Polka.manager_alloc_loose ()
-  let name = "Polyhedra Manager"
+  let name () = "Polyhedra"
 end
 
 (** Manager for the Box domain, i.e. an interval domain.
@@ -64,10 +64,10 @@ struct
   type mt = Box.t
   type t = mt Manager.t
   let mgr = Box.manager_alloc ()
-  let name = "Interval Manager"
+  let name () = "Interval"
 end
 
-let priv_manager =
+let manager =
   lazy (
     let options =
       ["octagon", (module OctagonManager: Manager);
@@ -81,7 +81,7 @@ let priv_manager =
   )
 
 let get_manager (): (module Manager) =
-  Lazy.force priv_manager
+  Lazy.force manager
 
 module type Tracked =
 sig
@@ -239,11 +239,28 @@ struct
 
   let copy = A.copy Man.mgr
 
-  let vars d =
+  let vars_as_array d =
     let ivs, fvs = Environment.vars (A.env d) in
     assert (Array.length fvs = 0); (* shouldn't ever contain floats *)
+    ivs
+
+  let vars d =
+    let ivs = vars_as_array d in
     List.of_enum (Array.enum ivs)
 
+  (* marshal type: Abstract0.t and an array of var names *)
+  type marshal = Man.mt Abstract0.t * string array
+
+  let unmarshal ((abstract0, vs): marshal): t =
+    let vars = Array.map Var.of_string vs in
+    (* We do not have real-valued vars, so we pass an empty array in their place. *)
+    let env = Environment.make vars [||] in
+    {abstract0; env}
+
+  let marshal (x: t): marshal =
+    let vars = Array.map Var.to_string (vars_as_array x) in
+    x.abstract0, vars
+
   let mem_var d v = Environment.mem_var (A.env d) v
 
   let add_vars_with nd vs =
@@ -465,6 +482,12 @@ struct
     let earray = Tcons1.array_make (A.env d) 1 in
     Tcons1.array_set earray 0 tcons1;
     A.meet_tcons_array Man.mgr d earray
+
+  let to_lincons_array d =
+    A.to_lincons_array Man.mgr d
+
+  let of_lincons_array (a: Apron.Lincons1.earray) =
+    A.of_lincons_array Man.mgr a.array_env a
 end
 
 
@@ -681,6 +704,8 @@ module DHetero (Man: Manager): SLattice with type t = Man.mt A.t =
 struct
   include DBase (Man)
 
+
+
   let gce (x: Environment.t) (y: Environment.t): Environment.t =
     let (xi, xf) = Environment.vars x in
     (* TODO: check type compatibility *)
@@ -835,7 +860,7 @@ end
 
 type ('a, 'b) aproncomponents_t = { apr : 'a; priv : 'b; } [@@deriving eq, ord, to_yojson]
 
-module D2 (Man: Manager) : S2 =
+module D2 (Man: Manager) : S2 with module Man = Man =
 struct
   include DWithOps (Man) (DHetero (Man))
   module Man = Man

src/cdomains/lockDomain.ml

@@ -140,7 +140,11 @@ struct
     let no_casts = S.map Expcompare.stripCastsDeepForPtrArith (eq_set ask e) in
     let addrs = S.filter (function AddrOf _ -> true | _ -> false) no_casts in
     S.union addrs st
-  let remove ask e st = S.diff st (eq_set ask e)
+  let remove ask e st = 
+    (* TODO: Removing based on must-equality sets is not sound! *)
+    let no_casts = S.map Expcompare.stripCastsDeepForPtrArith (eq_set ask e) in
+    let addrs = S.filter (function AddrOf _ -> true | _ -> false) no_casts in
+    S.diff st addrs
   let remove_var v st = S.filter (fun x -> not (Exp.contains_var v x)) st
 
   let kill_lval (host,offset) st =

src/dune

@@ -12,7 +12,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (wrapped false)
-  (modules :standard \ goblint mainarinc maindomaintest mainspec privPrecCompare)
+  (modules :standard \ goblint mainarinc maindomaintest mainspec privPrecCompare apronPrecCompare)
   (libraries goblint-cil.all-features batteries.unthreaded zarith_stubs_js qcheck-core.runner dune-site
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
@@ -21,6 +21,10 @@
       (apron apron.octMPQ apron.boxMPQ apron.polkaMPQ -> apronDomain.apron.ml)
       (-> apronDomain.no-apron.ml)
     )
+    (select apronPrecCompareUtil.ml from
+      (apron -> apronPrecCompareUtil.apron.ml)
+      (-> apronPrecCompareUtil.no-apron.ml)
+    )
     (select apronAnalysis.ml from
       (apron -> apronAnalysis.apron.ml)
       (-> apronAnalysis.no-apron.ml)
@@ -44,6 +48,7 @@
 ; TODO: Remove workaround with dune 3.0, where this should get fixed.
 (copy_files cdomains/apron/*.ml)
 (copy_files analyses/apron/*.ml)
+(copy_files util/apron/*.ml)
 (copy_files witness/z3/*.ml)
 
 (executables
@@ -64,6 +69,14 @@
   (flags :standard -linkall)
 )
 
+(executable
+  (name apronPrecCompare)
+  (modules apronPrecCompare)
+  (libraries goblint.lib)
+  (preprocess (staged_pps ppx_deriving.std ppx_deriving_yojson ppx_distr_guards ocaml-monadic))
+  (flags :standard -linkall)
+)
+
 (rule
   (targets goblint.ml config.ml version.ml)
   (mode fallback) ; do nothing if all targets already exist

src/framework/analyses.ml

@@ -238,7 +238,7 @@ struct
       let p_list p f xs = BatList.print ~first:"[\n  " ~last:"\n]" ~sep:",\n  " p f xs in
       (*let p_kv f (k,p,v) = fprintf f "\"%s\": %a" k p v in*)
       (*let p_obj f xs = BatList.print ~first:"{\n  " ~last:"\n}" ~sep:",\n  " p_kv xs in*)
-      let p_node f n = BatPrintf.fprintf f "%s" (Node.show_id n) in
+      let p_node f n = BatPrintf.fprintf f "\"%s\"" (Node.show_id n) in
       let p_fun f x = fprintf f "{\n  \"name\": \"%s\",\n  \"nodes\": %a\n}" x (p_list p_node) (SH.find_all funs2node x) in
       (*let p_fun f x = p_obj f [ "name", BatString.print, x; "nodes", p_list p_node, SH.find_all funs2node x ] in*)
       let p_file f x = fprintf f "{\n  \"name\": \"%s\",\n  \"path\": \"%s\",\n  \"functions\": %a\n}" (Filename.basename x) x (p_list p_fun) (SH.find_all file2funs x) in

src/privPrecCompare.ml

@@ -1,45 +1,6 @@
-open! Defaults (* CircInterval / Enums / ... need initialized conf *)
-open! Batteries
-open Prelude
-open Ana
-open PrivPrecCompareUtil
-open PrecCompare
-
-module VD = BaseDomain.VD
-
-let load filename =
-  let f = open_in_bin filename in
-  let dump: dump = Marshal.from_channel f in
-  close_in_noerr f;
-  dump
-
-module CompareDump = MakeHashtbl (LV) (VD) (LVH)
-
-let compare_dumps {name = name1; lvh = lvh1} {name = name2; lvh = lvh2} =
-  CompareDump.compare ~name1 lvh1 ~name2 lvh2
-
-let count_locations dumps =
-  let module LH = Hashtbl.Make (CilType.Location) in
-  let locations = LH.create 113 in
-  let location_vars = LVH.create 113 in
-  List.iter (fun {lvh; _} ->
-      LVH.iter (fun (l, x) _ ->
-          LH.replace locations l ();
-          LVH.replace location_vars (l, x) ()
-        ) lvh
-    ) dumps;
-  (LH.length locations, LVH.length location_vars)
+(* Utility program to compare precision of results of the base analysis with different privatizations *)
+(* The result files that can be compared here may be created by passing an output file name in "exp.priv-prec-dump" to Goblint *)
+module A = PrecCompare.MakeDump (PrivPrecCompareUtil)
 
 let () =
-  Cil.initCIL (); (* ValueDomain.Compound.leq depends on ptrdiffType initialization *)
-  let filenames = List.tl (Array.to_list Sys.argv) in
-  let dumps = List.map load filenames in
-  let (locations_count, location_vars_count) = count_locations dumps in
-  let i_dumps = List.mapi (fun i dump -> (i, dump)) dumps in
-  List.cartesian_product i_dumps i_dumps
-  (* |> List.filter (fun ((i1, _), (i2, _)) -> i1 < i2) *)
-  |> List.filter (fun ((i1, _), (i2, _)) -> i1 <> i2)
-  |> List.map (Tuple2.map snd snd)
-  |> List.map (uncurry compare_dumps)
-  |> List.iter (fun (_, msg) -> ignore (Pretty.printf "%t\n" (fun () -> msg)));
-  ignore (Pretty.printf "\nTotal locations: %d\nTotal location variables: %d\n" locations_count location_vars_count)
+  A.main ()