Use 'v type parameter in ctx operations for global constraint variabl…

…es (issue #469)

src/analyses/mCP.ml

@@ -237,6 +237,7 @@ struct
   module V = DomListPrintable (VarListSpec)
 
   open List open Obj
+  let v_of n v = [(n, repr v)]
 
   let name () = "MCP2"
 
@@ -389,14 +390,14 @@ struct
     if not (get_bool "exp.single-threaded") then
       iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs
 
-  let do_sideg ctx (xs:(varinfo * (int * Obj.t)) list) =
+  let do_sideg ctx (xs:(V.t * (int * Obj.t)) list) =
     let side_one v d =
       let join_vals (n,(module S:MCPSpec),d) =
         n, repr @@ fold_left (fun x y -> S.G.join x (obj y)) (S.G.bot ()) d
       in
       ctx.sideg v @@ topo_sort_an @@ map join_vals @@ spec_list @@ group_assoc (d @ G.bot ())
     in
-    iter (uncurry side_one) @@ group_assoc_eq Basetype.Variables.equal xs
+    iter (uncurry side_one) @@ group_assoc_eq V.equal xs
 
   let do_assigns ctx assigns (xs:(int * Obj.t) list) =
     if List.is_empty assigns then xs (* nothing to do *)
@@ -464,10 +465,10 @@ struct
             ; emit   = (fun e -> emits := e :: !emits)
             ; presub = filter_presubs n ctx.local
             ; postsub= filter_presubs n post_all
-            ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+            ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
             ; spawn  = (fun l v a  -> spawns := (v,(n,l,a)) :: !spawns)
             ; split  = (fun d es   -> splits := (n,(repr d,es)) :: !splits)
-            ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+            ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
             ; assign = (fun ?name v e    -> assigns := (v,e,name, repr ctx')::!assigns)
             }
           in
@@ -482,10 +483,10 @@ struct
             ; emit   = (fun e -> emits := e :: !emits)
             ; presub = filter_presubs n octx.local
             ; postsub= filter_presubs n post_all
-            ; global = (fun v      -> octx.global v |> assoc n |> obj)
+            ; global = (fun v      -> octx.global (v_of n v) |> assoc n |> obj)
             ; spawn  = (fun l v a  -> spawns := (v,(n,l,a)) :: !spawns)
             ; split  = (fun d es   -> splits := (n,(repr d,es)) :: !splits)
-            ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+            ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
             ; assign = (fun ?name v e    -> assigns := (v,e,name, repr octx')::!assigns)
             }
           in
@@ -521,10 +522,10 @@ struct
         ; emit   = (fun e -> emits := e :: !emits)
         ; presub = filter_presubs n ctx.local
         ; postsub= filter_presubs n post_all
-        ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun l v a  -> spawns := (v,(n,l,a)) :: !spawns)
         ; split  = (fun d es   -> splits := (n,(repr d,es)) :: !splits)
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name v e    -> assigns := (v,e,name, repr ctx')::!assigns)
         }
       in
@@ -558,10 +559,10 @@ struct
           ; emit   = (fun _ -> failwith "Cannot \"emit\" in query context.")
           ; presub = filter_presubs n ctx.local
           ; postsub= []
-          ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+          ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
           ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in query context.")
           ; split  = (fun d es   -> failwith "Cannot \"split\" in query context.")
-          ; sideg  = (fun v g    -> sides := (v, (n, repr g)) :: !sides)
+          ; sideg  = (fun v g    -> sides := (v_of n v, (n, repr g)) :: !sides)
           (* sideg is discouraged in query, because they would bypass sides grouping in other transfer functions.
              See https://github.com/goblint/analyzer/pull/214. *)
           ; assign = (fun ?name _ -> failwith "Cannot \"assign\" in query context.")
@@ -603,10 +604,10 @@ struct
         ; emit   = (fun e -> emits := e :: !emits)
         ; presub = filter_presubs n ctx.local
         ; postsub= filter_presubs n post_all
-        ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun l v a  -> spawns := (v,(n,l,a)) :: !spawns)
         ; split  = (fun d es   -> splits := (n,(repr d,es)) :: !splits)
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name _ -> failwith "Cannot \"assign\" in assign context (cycles?).")
         }
       in
@@ -637,10 +638,10 @@ struct
         ; emit   = (fun e -> emits := e :: !emits)
         ; presub = filter_presubs n ctx.local
         ; postsub= filter_presubs n post_all
-        ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun l v a  -> spawns := (v,(n,l,a)) :: !spawns)
         ; split  = (fun d es   -> splits := (n,(repr d,es)) :: !splits)
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name _ -> failwith "Cannot \"assign\" in assign context (cycles?).")
         }
       in
@@ -671,10 +672,10 @@ struct
         ; emit   = (fun e -> emits := e :: !emits)
         ; presub = filter_presubs n ctx.local
         ; postsub= filter_presubs n post_all
-        ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun l v a  -> spawns := (v,(n,l,a)) :: !spawns)
         ; split  = (fun d es   -> splits := (n,(repr d,es)) :: !splits)
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name v e -> assigns := (v,e,name, repr ctx')::!assigns)
         }
       in
@@ -706,10 +707,10 @@ struct
         ; emit   = (fun e -> emits := e :: !emits)
         ; presub = filter_presubs n ctx.local
         ; postsub= filter_presubs n post_all
-        ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun l v a  -> spawns := (v,(n,l,a)) :: !spawns)
         ; split  = (fun d es   -> splits := (n,(repr d,es)) :: !splits)
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name v e -> assigns := (v,e,name, repr ctx')::!assigns)
         }
       in
@@ -741,10 +742,10 @@ struct
         ; emit   = (fun e -> emits := e :: !emits)
         ; presub = filter_presubs n ctx.local
         ; postsub= filter_presubs n post_all
-        ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun l v a  -> spawns := (v,(n,l,a)) :: !spawns)
         ; split  = (fun d es   -> splits := (n,(repr d,es)) :: !splits)
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name v e -> assigns := (v,e,name, repr ctx')::!assigns)
         }
       in
@@ -776,10 +777,10 @@ struct
         ; emit   = (fun e -> emits := e :: !emits)
         ; presub = filter_presubs n ctx.local
         ; postsub= filter_presubs n post_all
-        ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun l v a  -> spawns := (v,(n,l,a)) :: !spawns)
         ; split  = (fun d es   -> splits := (n,(repr d,es)) :: !splits)
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name v e -> assigns := (v,e,name, repr ctx')::!assigns)
         }
       in
@@ -811,10 +812,10 @@ struct
         ; emit   = (fun e -> emits := e :: !emits)
         ; presub = filter_presubs n ctx.local
         ; postsub= filter_presubs n post_all
-        ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun l v a  -> spawns := (v,(n,l,a)) :: !spawns)
         ; split  = (fun d es   -> splits := (n,(repr d,es)) :: !splits)
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name v e -> assigns := (v,e,name, repr ctx')::!assigns)
         }
       in
@@ -846,10 +847,10 @@ struct
         ; emit   = (fun e -> emits := e :: !emits)
         ; presub = filter_presubs n ctx.local
         ; postsub= filter_presubs n post_all
-        ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun l v a  -> spawns := (v,(n,l,a)) :: !spawns)
         ; split  = (fun d es   -> splits := (n,(repr d,es)) :: !splits)
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name v e -> assigns := (v,e,name, repr ctx')::!assigns)
         }
       in
@@ -880,10 +881,10 @@ struct
         ; emit   = (fun e -> emits := e :: !emits)
         ; presub = filter_presubs n ctx.local
         ; postsub= filter_presubs n post_all
-        ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun l v a  -> spawns := (v,(n,l,a)) :: !spawns)
         ; split  = (fun d es   -> splits := (n,(repr d,es)) :: !splits)
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name _ -> failwith "Cannot \"assign\" in sync context.")
         }
       in
@@ -911,10 +912,10 @@ struct
         ; emit   = (fun _ -> failwith "Cannot \"emit\" in enter context.")
         ; presub = filter_presubs n ctx.local
         ; postsub= []
-        ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun l v a  -> spawns := (v,(n,l,a)) :: !spawns)
         ; split  = (fun _ _    -> failwith "Cannot \"split\" in enter context." )
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name _ -> failwith "Cannot \"assign\" in enter context.")
         }
       in
@@ -942,10 +943,10 @@ struct
         ; emit   = (fun e -> emits := e :: !emits)
         ; presub = filter_presubs n ctx.local
         ; postsub= filter_presubs n post_all
-        ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun l v a  -> spawns := (v,(n,l,a)) :: !spawns)
         ; split  = (fun d es   -> failwith "Cannot \"split\" in combine context.")
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name v e -> assigns := (v,e,name, repr ctx')::!assigns)
         }
       in
@@ -973,10 +974,10 @@ struct
         ; emit   = (fun e -> emits := e :: !emits)
         ; presub = filter_presubs n ctx.local
         ; postsub= []
-        ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in threadenter context.")
         ; split  = (fun d es   -> failwith "Cannot \"split\" in threadenter context.")
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name v e -> failwith "Cannot \"assign\" in threadenter context.")
         }
       in
@@ -1002,10 +1003,10 @@ struct
         ; emit   = (fun e -> emits := e :: !emits)
         ; presub = filter_presubs n ctx.local
         ; postsub= filter_presubs n post_all
-        ; global = (fun v      -> ctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> ctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in threadspawn context.")
         ; split  = (fun d es   -> failwith "Cannot \"split\" in threadspawn context.")
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name v e -> failwith "Cannot \"assign\" in threadspawn context.")
         }
       in
@@ -1020,10 +1021,10 @@ struct
         ; emit   = (fun e -> emits := e :: !emits)
         ; presub = filter_presubs n fctx.local
         ; postsub= filter_presubs n post_all
-        ; global = (fun v      -> fctx.global v |> assoc n |> obj)
+        ; global = (fun v      -> fctx.global (v_of n v) |> assoc n |> obj)
         ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in threadspawn context.")
         ; split  = (fun d es   -> failwith "Cannot \"split\" in threadspawn context.")
-        ; sideg  = (fun v g    -> sides  := (v, (n, repr g)) :: !sides)
+        ; sideg  = (fun v g    -> sides  := (v_of n v, (n, repr g)) :: !sides)
         ; assign = (fun ?name v e -> failwith "Cannot \"assign\" in threadspawn context.")
         }
       in

src/domains/printable.ml

@@ -41,7 +41,7 @@ struct
 
   (* start MapDomain.Groupable *)
   type group = |
-  let show_group (x: group)= match x with _ -> .
+  let show_group (x: group) = match x with _ -> .
   let to_group _ = None
   let trace_enabled = false
   (* end MapDomain.Groupable *)

src/framework/analyses.ml

@@ -66,8 +66,18 @@ struct
   let var_id (n,_) = Var.var_id n
   let node (n,_) = n
 end
-exception Deadcode
 
+module GVarF (V: Printable.S) =
+struct
+  include V
+  (* from Basetype.Variables *)
+  let var_id _ = "globals"
+  let node _ = MyCFG.Function Cil.dummyFunDec
+  let pretty_trace = pretty
+end
+
+
+exception Deadcode
 
 (** [Dom (D)] produces D lifted where bottom means dead-code *)
 module Dom (LD: Lattice.S) =
@@ -286,12 +296,12 @@ type ('d,'g,'c,'v) ctx =
   ; context  : unit -> 'c (** current Spec context *)
   ; edge     : MyCFG.edge
   ; local    : 'd
-  ; global   : varinfo -> 'g
+  ; global   : 'v -> 'g
   ; presub   : (string * Obj.t) list
   ; postsub  : (string * Obj.t) list
   ; spawn    : lval option -> varinfo -> exp list -> unit
   ; split    : 'd -> Events.t list -> unit
-  ; sideg    : varinfo -> 'g -> unit
+  ; sideg    : 'v -> 'g -> unit
   ; assign   : ?name:string -> lval -> exp -> unit
   }
 

src/framework/constraints.ml

@@ -456,10 +456,11 @@ end
 module FromSpec (S:Spec) (Cfg:CfgBackward) (I: Increment)
   : sig
     include GlobConstrSys with module LVar = VarF (S.C)
-                           and module GVar = Basetype.Variables
+                           (* and module GVar = Basetype.Variables *)
+                           and module GVar = GVarF (S.V)
                            and module D = S.D
                            and module G = S.G
-    val tf : MyCFG.node * S.C.t -> (Cil.location * MyCFG.edge) list * MyCFG.node -> ((MyCFG.node * S.C.t) -> S.D.t) -> (MyCFG.node * S.C.t -> S.D.t -> unit) -> (Cil.varinfo -> G.t) -> (Cil.varinfo -> G.t -> unit) -> D.t
+    val tf : MyCFG.node * S.C.t -> (Cil.location * MyCFG.edge) list * MyCFG.node -> ((MyCFG.node * S.C.t) -> S.D.t) -> (MyCFG.node * S.C.t -> S.D.t -> unit) -> (GVar.t -> G.t) -> (GVar.t -> G.t -> unit) -> D.t
   end
 =
 struct
@@ -468,7 +469,8 @@ struct
   type ld = S.D.t
   (* type gd = S.G.t *)
   module LVar = VarF (S.C)
-  module GVar = Basetype.Variables
+  (* module GVar = Basetype.Variables *)
+  module GVar = GVarF (S.V)
   module D = S.D
   module G = S.G
 
@@ -1071,7 +1073,8 @@ end
 module Compare
     (S:Spec)
     (Sys:GlobConstrSys with module LVar = VarF (S.C)
-                        and module GVar = Basetype.Variables
+                        (* and module GVar = Basetype.Variables *)
+                        and module GVar = GVarF (S.V)
                         and module D = S.D
                         and module G = S.G)
     (LH:Hashtbl.S with type key=Sys.LVar.t)

src/framework/control.ml

@@ -187,7 +187,7 @@ struct
     let make_global_fast_xml f g =
       let open Printf in
       let print_globals k v =
-        fprintf f "\n<glob><key>%s</key>%a</glob>" (XmlUtil.escape (Basetype.Variables.show k)) Spec.G.printXml v;
+        fprintf f "\n<glob><key>%s</key>%a</glob>" (XmlUtil.escape (Spec.V.show k)) Spec.G.printXml v;
       in
       GHT.iter print_globals g
     in
@@ -215,7 +215,7 @@ struct
     let gh = GHT.create 13 in
     let getg v = GHT.find_default gh v (Spec.G.bot ()) in
     let sideg v d =
-      if M.tracing then M.trace "global_inits" "sideg %a = %a\n" Prelude.Ana.d_varinfo v Spec.G.pretty d;
+      if M.tracing then M.trace "global_inits" "sideg %a = %a\n" Spec.V.pretty v Spec.G.pretty d;
       GHT.replace gh v (Spec.G.join (getg v) d)
     in
     (* Old-style global function for context.

src/witness/witness.ml

@@ -269,7 +269,8 @@ open Analyses
 module Result (Cfg : CfgBidir)
               (Spec : Spec)
               (EQSys : GlobConstrSys with module LVar = VarF (Spec.C)
-                                  and module GVar = Basetype.Variables
+                                  (* and module GVar = Basetype.Variables *)
+                                  and module GVar = GVarF (Spec.V)
                                   and module D = Spec.D
                                   and module G = Spec.G)
               (LHT : BatHashtbl.S with type key = EQSys.LVar.t)