Add 'v type parameter to ctx for global constraint variables (issue #469

)
goblint · Dec 1, 2021 · 8b03bf4 · 8b03bf4
1 parent 09ff824
commit 8b03bf4
Show file tree

Hide file tree

Showing 10 changed files with 60 additions and 60 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -1884,7 +1884,7 @@ struct
     set_many ?ctx ask gs st invalids'
 
 
-  let make_entry ?(thread=false) (ctx:(D.t, G.t, C.t) Analyses.ctx) fundec args: D.t =
+  let make_entry ?(thread=false) (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) fundec args: D.t =
     let st: store = ctx.local in
     (* Evaluate the arguments. *)
     let vals = List.map (eval_rv (Analyses.ask_of_ctx ctx) ctx.global st) args in
@@ -1929,7 +1929,7 @@ struct
 
 
 
-  let forkfun (ctx:(D.t, G.t, C.t) Analyses.ctx) (lv: lval option) (f: varinfo) (args: exp list) : (lval option * varinfo * exp list) list =
+  let forkfun (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) (lv: lval option) (f: varinfo) (args: exp list) : (lval option * varinfo * exp list) list =
     let create_thread lval arg v =
       try
         (* try to get function declaration *)

diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
@@ -453,7 +453,7 @@ struct
         let assigns = ref [] in
         let emits = ref [] in
         let f post_all (n,(module S:MCPSpec),d) =
-          let rec ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+          let rec ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
             { local  = obj d
             ; node   = ctx.node
             ; prev_node = ctx.prev_node
@@ -471,7 +471,7 @@ struct
             ; assign = (fun ?name v e    -> assigns := (v,e,name, repr ctx')::!assigns)
             }
           in
-          let rec octx' : (S.D.t, S.G.t, S.C.t) ctx =
+          let rec octx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
             { local  = obj (assoc n octx.local)
             ; node   = octx.node
             ; prev_node = octx.prev_node
@@ -503,14 +503,14 @@ struct
     let ctx' = List.fold_left do_emit (ctx_with_local ctx xs) emits in
     ctx'.local
 
-  and branch (ctx:(D.t, G.t, C.t) ctx) (e:exp) (tv:bool) =
+  and branch (ctx:(D.t, G.t, C.t, V.t) ctx) (e:exp) (tv:bool) =
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in (* why do we need to collect these instead of calling ctx.sideg directly? *)
     let assigns = ref [] in
     let emits = ref [] in
     let f post_all (n,(module S:MCPSpec),d) =
-      let rec ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let rec ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj d
         ; node   = ctx.node
         ; prev_node = ctx.prev_node
@@ -539,15 +539,15 @@ struct
     if q then raise Deadcode else d
 
   (* Explicitly polymorphic type required here for recursive GADT call in ask. *)
-  and query': type a. QuerySet.t -> (D.t, G.t, C.t) ctx -> a Queries.t -> a Queries.result = fun asked ctx q ->
+  and query': type a. QuerySet.t -> (D.t, G.t, C.t, V.t) ctx -> a Queries.t -> a Queries.result = fun asked ctx q ->
     let module Result = (val Queries.Result.lattice q) in
     if QuerySet.mem (Any q) asked then
       Result.top () (* query cycle *)
     else
       let asked' = QuerySet.add (Any q) asked in
       let sides = ref [] in
       let f a (n,(module S:MCPSpec),d) =
-        let ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+        let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
           { local  = obj d
           ; node   = ctx.node
           ; prev_node = ctx.prev_node
@@ -583,16 +583,16 @@ struct
         do_sideg ctx !sides;
         r
 
-  and query: type a. (D.t, G.t, C.t) ctx -> a Queries.t -> a Queries.result = fun ctx q ->
+  and query: type a. (D.t, G.t, C.t, V.t) ctx -> a Queries.t -> a Queries.result = fun ctx q ->
     query' QuerySet.empty ctx q
 
-  let assign (ctx:(D.t, G.t, C.t) ctx) l e =
+  let assign (ctx:(D.t, G.t, C.t, V.t) ctx) l e =
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in
     let emits = ref [] in
     let f post_all (n,(module S:MCPSpec),d) =
-      let ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj d
         ; node   = ctx.node
         ; prev_node = ctx.prev_node
@@ -620,13 +620,13 @@ struct
     if q then raise Deadcode else d
 
 
-  let vdecl (ctx:(D.t, G.t, C.t) ctx) v =
+  let vdecl (ctx:(D.t, G.t, C.t, V.t) ctx) v =
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in
     let emits = ref [] in
     let f post_all (n,(module S:MCPSpec),d) =
-      let ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj d
         ; node   = ctx.node
         ; prev_node = ctx.prev_node
@@ -653,14 +653,14 @@ struct
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
-  let body (ctx:(D.t, G.t, C.t) ctx) f =
+  let body (ctx:(D.t, G.t, C.t, V.t) ctx) f =
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in
     let assigns = ref [] in
     let emits = ref [] in
     let f post_all (n,(module S:MCPSpec),d) =
-      let rec ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let rec ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj d
         ; node   = ctx.node
         ; prev_node = ctx.prev_node
@@ -688,14 +688,14 @@ struct
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
-  let return (ctx:(D.t, G.t, C.t) ctx) e f =
+  let return (ctx:(D.t, G.t, C.t, V.t) ctx) e f =
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in
     let assigns = ref [] in
     let emits = ref [] in
     let f post_all (n,(module S:MCPSpec),d) =
-      let rec ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let rec ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj d
         ; node   = ctx.node
         ; prev_node = ctx.prev_node
@@ -723,14 +723,14 @@ struct
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
-  let intrpt (ctx:(D.t, G.t, C.t) ctx) =
+  let intrpt (ctx:(D.t, G.t, C.t, V.t) ctx) =
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in
     let assigns = ref [] in
     let emits = ref [] in
     let f post_all (n,(module S:MCPSpec),d) =
-      let rec ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let rec ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj d
         ; node   = ctx.node
         ; prev_node = ctx.prev_node
@@ -758,14 +758,14 @@ struct
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
-  let asm (ctx:(D.t, G.t, C.t) ctx) =
+  let asm (ctx:(D.t, G.t, C.t, V.t) ctx) =
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in
     let assigns = ref [] in
     let emits = ref [] in
     let f post_all (n,(module S:MCPSpec),d) =
-      let rec ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let rec ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj d
         ; node   = ctx.node
         ; prev_node = ctx.prev_node
@@ -793,14 +793,14 @@ struct
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
-  let skip (ctx:(D.t, G.t, C.t) ctx) =
+  let skip (ctx:(D.t, G.t, C.t, V.t) ctx) =
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in
     let assigns = ref [] in
     let emits = ref [] in
     let f post_all (n,(module S:MCPSpec),d) =
-      let rec ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let rec ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj d
         ; node   = ctx.node
         ; prev_node = ctx.prev_node
@@ -828,14 +828,14 @@ struct
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
-  let special (ctx:(D.t, G.t, C.t) ctx) r f a =
+  let special (ctx:(D.t, G.t, C.t, V.t) ctx) r f a =
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in
     let assigns = ref [] in
     let emits = ref [] in
     let f post_all (n,(module S:MCPSpec),d) =
-      let rec ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let rec ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj d
         ; node   = ctx.node
         ; prev_node = ctx.prev_node
@@ -863,13 +863,13 @@ struct
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
-  let sync (ctx:(D.t, G.t, C.t) ctx) reason =
+  let sync (ctx:(D.t, G.t, C.t, V.t) ctx) reason =
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in
     let emits = ref [] in
     let f post_all (n,(module S:MCPSpec),d) =
-      let ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj d
         ; node   = ctx.node
         ; prev_node = ctx.prev_node
@@ -896,11 +896,11 @@ struct
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
-  let enter (ctx:(D.t, G.t, C.t) ctx) r f a =
+  let enter (ctx:(D.t, G.t, C.t, V.t) ctx) r f a =
     let spawns = ref [] in
     let sides  = ref [] in
     let f (n,(module S:MCPSpec),d) =
-      let ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj d
         ; node   = ctx.node
         ; prev_node = ctx.prev_node
@@ -925,13 +925,13 @@ struct
     do_spawns ctx !spawns;
     map (fun xs -> (topo_sort_an @@ map fst xs, topo_sort_an @@ map snd xs)) @@ n_cartesian_product css
 
-  let combine (ctx:(D.t, G.t, C.t) ctx) r fe f a fc fd =
+  let combine (ctx:(D.t, G.t, C.t, V.t) ctx) r fe f a fc fd =
     let spawns = ref [] in
     let sides  = ref [] in
     let assigns = ref [] in
     let emits = ref [] in
     let f post_all (n,(module S:MCPSpec),d) =
-      let rec ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let rec ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj d
         ; node   = ctx.node
         ; prev_node = ctx.prev_node
@@ -958,11 +958,11 @@ struct
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
-  let threadenter (ctx:(D.t, G.t, C.t) ctx) lval f a =
+  let threadenter (ctx:(D.t, G.t, C.t, V.t) ctx) lval f a =
     let sides  = ref [] in
     let emits = ref [] in
     let f (n,(module S:MCPSpec),d) =
-      let ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj d
         ; node   = ctx.node
         ; prev_node = ctx.prev_node
@@ -987,11 +987,11 @@ struct
     (* TODO: this do_emits is now different from everything else *)
     map (do_emits ctx !emits) @@ map topo_sort_an @@ n_cartesian_product css
 
-  let threadspawn (ctx:(D.t, G.t, C.t) ctx) lval f a fctx =
+  let threadspawn (ctx:(D.t, G.t, C.t, V.t) ctx) lval f a fctx =
     let sides  = ref [] in
     let emits = ref [] in
     let f post_all (n,(module S:MCPSpec),d) =
-      let ctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj d
         ; node   = ctx.node
         ; prev_node = ctx.prev_node
@@ -1009,7 +1009,7 @@ struct
         ; assign = (fun ?name v e -> failwith "Cannot \"assign\" in threadspawn context.")
         }
       in
-      let fctx' : (S.D.t, S.G.t, S.C.t) ctx =
+      let fctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
         { local  = obj (assoc n fctx.local)
         ; node   = fctx.node
         ; prev_node = fctx.prev_node

diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml
@@ -71,7 +71,7 @@ struct
   type marshal = NodeVarinfoMap.marshal
 
   let get_heap_var = NodeVarinfoMap.to_varinfo
-  let query (ctx: (D.t, G.t, C.t) ctx) (type a) (q: a Q.t): a Queries.result =
+  let query (ctx: (D.t, G.t, C.t, V.t) ctx) (type a) (q: a Q.t): a Queries.result =
     match q with
     | Q.HeapVar ->
       let node = match ctx.local with

diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
@@ -144,7 +144,7 @@ struct
 
   let arinc_analysis_activated = ref false
 
-  let do_access (ctx: (D.t, G.t, C.t) ctx) (w:bool) (reach:bool) (conf:int) (e:exp) =
+  let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (w:bool) (reach:bool) (conf:int) (e:exp) =
     let open Queries in
     let part_access ctx (e:exp) (vo:varinfo option) (w: bool) =
       (*privatization*)

diff --git a/src/analyses/octagon.ml b/src/analyses/octagon.ml
@@ -245,7 +245,7 @@ struct
           start
     | None -> start
 
-  let make_entry (ctx:(D.t, G.t, C.t) Analyses.ctx) fn (args: exp list): D.t =
+  let make_entry (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) fn (args: exp list): D.t =
     (* The normal haskell zip that throws no exception *)
     let rec zip x y  = match x,y with
     | (x::xs), (y::ys) -> (x,y) :: zip xs ys

diff --git a/src/analyses/shapes.ml b/src/analyses/shapes.ml
@@ -61,7 +61,7 @@ struct
     in
     S.elements (cv e)
 
-  let re_context (ctx: (D.t,G.t,C.t) ctx) (re:Re.D.t): (Re.D.t, Re.G.t,C.t) ctx =
+  let re_context (ctx: (D.t,G.t,C.t,V.t) ctx) (re:Re.D.t): (Re.D.t, Re.G.t,C.t,V.t) ctx =
     let ge v = let a,b = ctx.global v in b in
     let spawn f v x = f v x in
     let geffect f v d = f v (false, d) in

diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
@@ -91,7 +91,7 @@ struct
     | `Lifted current -> BatOption.map_default (ConcDomain.ThreadSet.of_list) (ConcDomain.ThreadSet.top ()) (Thread.created current td)
     | _ -> ConcDomain.ThreadSet.top ()
 
-  let query (ctx: (D.t, _, _) ctx) (type a) (x: a Queries.t): a Queries.result =
+  let query (ctx: (D.t, _, _, _) ctx) (type a) (x: a Queries.t): a Queries.result =
     match x with
     | Queries.CurrentThreadId -> fst ctx.local
     | Queries.CreatedThreads -> created ctx.local

diff --git a/src/analyses/threadReturn.ml b/src/analyses/threadReturn.ml
@@ -43,7 +43,7 @@ struct
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
-  let query (ctx: (D.t, _, _) ctx) (type a) (x: a Queries.t): a Queries.result =
+  let query (ctx: (D.t, _, _, _) ctx) (type a) (x: a Queries.t): a Queries.result =
     match x with
     | Queries.MayBeThreadReturn -> ctx.local
     | _ -> Queries.Result.top x