Merge pull request #1283 from goblint/apron_libification

Simplify relational domains interface somewhat

src/analyses/apron/affineEqualityAnalysis.apron.ml

@@ -11,7 +11,6 @@ let spec_module: (module MCPSpec) Lazy.t =
     let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in
     let module RD: RelationDomain.RD =
     struct
-      module Var = AffineEqualityDomain.Var
       module V = AffineEqualityDomain.V
       include AD
     end

src/analyses/apron/apronAnalysis.apron.ml

@@ -12,10 +12,9 @@ let spec_module: (module MCPSpec) Lazy.t =
     let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): ApronDomain.S3) else (module AD)) in
     let module RD: RelationDomain.RD =
     struct
-      module Var = ApronDomain.Var
       module V = ApronDomain.V
       include AD
-      type var = ApronDomain.Var.t
+      type var = Apron.Var.t
     end
     in
     let module Priv = (val RelationPriv.get_priv ()) in

src/analyses/apron/relationAnalysis.apron.ml

@@ -285,7 +285,7 @@ struct
     (* there should be smarter ways to do this, e.g. by keeping track of which values are written etc. ... *)
     (* See, e.g, Beckschulze E, Kowalewski S, Brauer J (2012) Access-based localization for octagons. Electron Notes Theor Comput Sci 287:29–40 *)
     (* Also, a local *)
-    let vname = RD.Var.to_string var in
+    let vname = Apron.Var.to_string var in
     let locals = fundec.sformals @ fundec.slocals in
     match List.find_opt (fun v -> VM.var_name (Local v) = vname) locals with (* TODO: optimize *)
     | None -> true
@@ -318,7 +318,7 @@ struct
     RD.remove_filter_with new_rel (fun var ->
         match RV.find_metadata var with
         | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) -> true (* remove caller locals provided they are unreachable *)
-        | Some (Arg _) when not (List.mem_cmp RD.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *)
+        | Some (Arg _) when not (List.mem_cmp Apron.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *)
         | _ -> false (* keep everything else (just added args, globals, global privs) *)
       );
     if M.tracing then M.tracel "combine" "relation enter newd: %a\n" RD.pretty new_rel;
@@ -404,7 +404,7 @@ struct
     in
     let any_local_reachable = any_local_reachable fundec reachable_from_args in
     let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in
-    if M.tracing then M.tracel "combine" "relation remove vars: %a\n" (docList (fun v -> Pretty.text (RD.Var.to_string v))) arg_vars;
+    if M.tracing then M.tracel "combine" "relation remove vars: %a\n" (docList (fun v -> Pretty.text (Apron.Var.to_string v))) arg_vars;
     RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *)
     let tainted = f_ask.f Queries.MayBeTainted in
     let tainted_vars = TaintPartialContexts.conv_varset tainted in

src/analyses/apron/relationPriv.apron.ml

@@ -195,8 +195,7 @@ struct
   end
   module AV =
   struct
-    include RelationDomain.VarMetadataTbl (VM) (RD.Var)
-
+    include RelationDomain.VarMetadataTbl (VM)
 
     let local g = make_var (Local g)
     let unprot g = make_var (Unprot g)

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -10,7 +10,7 @@ open Batteries
 open GoblintCil
 open Pretty
 module M = Messages
-open Apron
+open GobApron
 open VectorMatrix
 
 module Mpqf = struct
@@ -26,14 +26,12 @@ module Mpqf = struct
   let hash x = 31 * (Z.hash (get_den x)) + Z.hash (get_num x)
 end
 
-module Var = SharedFunctions.Var
-module V = RelationDomain.V(Var)
+module V = RelationDomain.V
 
 (** It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars.
     Furthermore, it provides the function get_coeff_vec that parses an apron expression into a vector of coefficients if the apron expression has an affine form. *)
 module VarManagement (Vec: AbstractVector) (Mx: AbstractMatrix)=
 struct
-  include SharedFunctions.EnvOps
   module Vector = Vec (Mpqf)
   module Matrix = Mx(Mpqf) (Vec)
 
@@ -78,16 +76,18 @@ struct
 
   let change_d t new_env add del = timing_wrap "dimension change" (change_d t new_env add) del
 
+  let vars x = Environment.ivars_only x.env
+
   let add_vars t vars =
     let t = copy t in
-    let env' = add_vars t.env vars in
+    let env' = Environment.add_vars t.env vars in
     change_d t env' true false
 
   let add_vars t vars = timing_wrap "add_vars" (add_vars t) vars
 
   let drop_vars t vars del =
     let t = copy t in
-    let env' = remove_vars t.env vars in
+    let env' = Environment.remove_vars t.env vars in
     change_d t env' false del
 
   let drop_vars t vars = timing_wrap "drop_vars" (drop_vars t) vars
@@ -102,7 +102,7 @@ struct
     t.env <- t'.env
 
   let remove_filter t f =
-    let env' = remove_filter t.env f in
+    let env' = Environment.remove_filter t.env f in
     change_d t env' false false
 
   let remove_filter t f = timing_wrap "remove_filter" (remove_filter t) f
@@ -114,19 +114,18 @@ struct
 
   let keep_filter t f =
     let t = copy t in
-    let env' = keep_filter t.env f in
+    let env' = Environment.keep_filter t.env f in
     change_d t env' false false
 
   let keep_filter t f = timing_wrap "keep_filter" (keep_filter t) f
 
   let keep_vars t vs =
     let t = copy t in
-    let env' = keep_vars t.env vs in
+    let env' = Environment.keep_vars t.env vs in
     change_d t env' false false
 
   let keep_vars t vs = timing_wrap "keep_vars" (keep_vars t) vs
 
-  let vars t = vars t.env
 
   let mem_var t var = Environment.mem_var t.env var
 
@@ -462,6 +461,7 @@ struct
 
   let assign_exp (t: VarManagement(Vc)(Mx).t) var exp (no_ov: bool Lazy.t) =
     let t = if not @@ Environment.mem_var t.env var then add_vars t [var] else t in
+    (* TODO: Do we need to do a constant folding here? It happens for texpr1_of_cil_exp *)
     match Convert.texpr1_expr_of_cil_exp t t.env exp (Lazy.force no_ov) with
     | exp -> assign_texpr t var exp
     | exception Convert.Unsupported_CilExp _ ->

src/cdomains/apron/apronDomain.apron.ml

@@ -4,7 +4,7 @@ open Batteries
 open GoblintCil
 open Pretty
 (* A binding to a selection of Apron-Domains *)
-open Apron
+open GobApron
 open RelationDomain
 open SharedFunctions
 
@@ -29,8 +29,7 @@ let widening_thresholds_apron = ResettableLazy.from_fun (fun () ->
 let reset_lazy () =
   ResettableLazy.reset widening_thresholds_apron
 
-module Var = SharedFunctions.Var
-module V = RelationDomain.V(Var)
+module V = RelationDomain.V
 
 
 module type Manager =
@@ -209,7 +208,6 @@ module type AOpsExtra =
 sig
   type t
   val copy : t -> t
-  val vars_as_array : t -> Var.t array
   val vars : t -> Var.t list
   type marshal
   val unmarshal : marshal -> t
@@ -248,15 +246,6 @@ struct
 
   let copy = A.copy Man.mgr
 
-  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
 
@@ -266,31 +255,24 @@ struct
     let env = Environment.make vars [||] in
     {abstract0; env}
 
+  let vars x = Environment.ivars_only @@ A.env x
+
   let marshal (x: t): marshal =
-    let vars = Array.map Var.to_string (vars_as_array x) in
+    let vars = Array.map Var.to_string (Array.of_list (vars x)) in
     x.abstract0, vars
 
   let mem_var d v = Environment.mem_var (A.env d) v
 
-  let add_vars_with nd vs =
-    let env' = EnvOps.add_vars (A.env nd) vs in
+  let envop f nd a =
+    let env' = f (A.env nd) a in
     A.change_environment_with Man.mgr nd env' false
 
-  let remove_vars_with nd vs =
-    let env' = EnvOps.remove_vars (A.env nd) vs in
-    A.change_environment_with Man.mgr nd env' false
+  let add_vars_with = envop Environment.add_vars
+  let remove_vars_with = envop Environment.remove_vars
+  let remove_filter_with = envop Environment.remove_filter
+  let keep_vars_with = envop Environment.keep_vars
+  let keep_filter_with = envop Environment.keep_filter
 
-  let remove_filter_with nd f =
-    let env' = EnvOps.remove_filter (A.env nd) f in
-    A.change_environment_with Man.mgr nd env' false
-
-  let keep_vars_with nd vs =
-    let env' = EnvOps.keep_vars (A.env nd) vs in
-    A.change_environment_with Man.mgr nd env' false
-
-  let keep_filter_with nd f =
-    let env' = EnvOps.keep_filter (A.env nd) f in
-    A.change_environment_with Man.mgr nd env' false
 
   let forget_vars_with nd vs =
     (* Unlike keep_vars_with, this doesn't check mem_var, but assumes valid vars, like assigns *)
@@ -497,9 +479,9 @@ struct
   let to_yojson (x: t) =
     let constraints =
       A.to_lincons_array Man.mgr x
-      |> SharedFunctions.Lincons1Set.of_earray
-      |> SharedFunctions.Lincons1Set.elements
-      |> List.map (fun lincons1 -> `String (SharedFunctions.Lincons1.show lincons1))
+      |> Lincons1Set.of_earray
+      |> Lincons1Set.elements
+      |> List.map (fun lincons1 -> `String (Lincons1.show lincons1))
     in
     let env = `String (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x))
     in
@@ -886,7 +868,6 @@ struct
   let unmarshal (b, d) = (BoxD.unmarshal b, D.unmarshal d)
 
   let mem_var (_, d) v = D.mem_var d v
-  let vars_as_array (_, d) = D.vars_as_array d
   let vars (_, d) = D.vars d
 
   let pretty_diff () ((_, d1), (_, d2)) = D.pretty_diff () (d1, d2)

src/cdomains/apron/gobApron.apron.ml

@@ -0,0 +1,98 @@
+open Batteries
+include Apron
+
+module Var =
+struct
+  include Var
+  let equal x y = Var.compare x y = 0
+end
+
+module Lincons1 =
+struct
+  include Lincons1
+
+  let show = Format.asprintf "%a" print
+  let compare x y = String.compare (show x) (show y) (* HACK *)
+
+  let num_vars x =
+    (* Apron.Linexpr0.get_size returns some internal nonsense, so we count ourselves. *)
+    let size = ref 0 in
+    Lincons1.iter (fun coeff var ->
+        if not (Apron.Coeff.is_zero coeff) then
+          incr size
+      ) x;
+    !size
+end
+
+module Lincons1Set =
+struct
+  include Set.Make (Lincons1)
+
+  let of_earray ({lincons0_array; array_env}: Lincons1.earray): t =
+    Array.enum lincons0_array
+    |> Enum.map (fun (lincons0: Lincons0.t) ->
+        Lincons1.{lincons0; env = array_env}
+      )
+    |> of_enum
+end
+
+(** A few code elements for environment changes from functions as remove_vars etc. have been moved to sharedFunctions as they are needed in a similar way inside affineEqualityDomain.
+    A module that includes various methods used by variable handling operations such as add_vars, remove_vars etc. in apronDomain and affineEqualityDomain. *)
+module Environment =
+struct
+  include Environment
+
+  let ivars_only env =
+    let ivs, fvs = Environment.vars env in
+    assert (Array.length fvs = 0); (* shouldn't ever contain floats *)
+    List.of_enum (Array.enum ivs)
+
+  let add_vars env vs =
+    let vs' =
+      vs
+      |> List.enum
+      |> Enum.filter (fun v -> not (Environment.mem_var env v))
+      |> Array.of_enum
+    in
+    Environment.add env vs' [||]
+
+  let remove_vars env vs =
+    let vs' =
+      vs
+      |> List.enum
+      |> Enum.filter (fun v -> Environment.mem_var env v)
+      |> Array.of_enum
+    in
+    Environment.remove env vs'
+
+  let remove_filter env f =
+    let vs' =
+      ivars_only env
+      |> List.enum
+      |> Enum.filter f
+      |> Array.of_enum
+    in
+    Environment.remove env vs'
+
+  let keep_vars env vs =
+    (* Instead of iterating over all vars in env and doing a linear lookup in vs just to remove them,
+        make a new env with just the desired vs. *)
+    let vs' =
+      vs
+      |> List.enum
+      |> Enum.filter (fun v -> Environment.mem_var env v)
+      |> Array.of_enum
+    in
+    Environment.make vs' [||]
+
+  let keep_filter env f =
+    (* Instead of removing undesired vars,
+       make a new env with just the desired vars. *)
+    let vs' =
+      ivars_only env
+      |> List.enum
+      |> Enum.filter f
+      |> Array.of_enum
+    in
+    Environment.make vs' [||]
+end