Merge pull request #801 from goblint/control-c

Add static module for top-level Control Spec context

src/domains/printable.ml

@@ -567,6 +567,31 @@ struct
 end
 
 
+module type FailwithMessage =
+sig
+  val message: string
+end
+
+module Failwith (Message: FailwithMessage): S =
+struct
+  type t = |
+
+  let name () = "failwith"
+  let equal _ _ = failwith Message.message
+  let compare _ _ = failwith Message.message
+  let hash _ = failwith Message.message
+  let tag _ = failwith Message.message
+
+  let show _ = failwith Message.message
+  let pretty _ _ = failwith Message.message
+  let printXml _ _ = failwith Message.message
+  let to_yojson _ = failwith Message.message
+
+  let arbitrary _ = failwith Message.message
+  let relift _ = failwith Message.message
+end
+
+
 (** Concatenates a list of strings that
     fit in the given character constraint *)
 let get_short_list begin_str end_str list =

src/framework/analyses.ml

@@ -269,6 +269,63 @@ struct
 end
 
 
+(** Reference to top-level Control Spec context first-class module. *)
+let control_spec_c: (module Printable.S) ref =
+  let module Failwith = Printable.Failwith (
+    struct
+      let message = "uninitialized control_spec_c"
+    end
+    )
+  in
+  ref (module Failwith: Printable.S)
+
+(** Top-level Control Spec context as static module, which delegates to {!control_spec_c}.
+    This allows using top-level context values inside individual analyses. *)
+module ControlSpecC: Printable.S =
+struct
+  type t = Obj.t (** represents [(val !control_spec_c).t] *)
+
+  (* The extra level of indirection allows calls to this static module to go to a dynamic first-class module. *)
+
+  let name () =
+    let module C = (val !control_spec_c) in
+    C.name ()
+
+  let equal x y =
+    let module C = (val !control_spec_c) in
+    C.equal (Obj.obj x) (Obj.obj y)
+  let compare x y =
+    let module C = (val !control_spec_c) in
+    C.compare (Obj.obj x) (Obj.obj y)
+  let hash x =
+    let module C = (val !control_spec_c) in
+    C.hash (Obj.obj x)
+  let tag x =
+    let module C = (val !control_spec_c) in
+    C.tag (Obj.obj x)
+
+  let show x =
+    let module C = (val !control_spec_c) in
+    C.show (Obj.obj x)
+  let pretty () x =
+    let module C = (val !control_spec_c) in
+    C.pretty () (Obj.obj x)
+  let printXml f x =
+    let module C = (val !control_spec_c) in
+    C.printXml f (Obj.obj x)
+  let to_yojson x =
+    let module C = (val !control_spec_c) in
+    C.to_yojson (Obj.obj x)
+
+  let arbitrary () =
+    let module C = (val !control_spec_c) in
+    QCheck.map ~rev:Obj.obj Obj.repr (C.arbitrary ())
+  let relift x =
+    let module C = (val !control_spec_c) in
+    Obj.repr (C.relift (Obj.obj x))
+end
+
+
 (* Experiment to reduce the number of arguments on transfer functions and allow
    sub-analyses. The list sub contains the current local states of analyses in
    the same order as written in the dependencies list (in MCP).
@@ -284,8 +341,8 @@ type ('d,'g,'c,'v) ctx =
   ; emit     : Events.t -> unit
   ; node     : MyCFG.node
   ; prev_node: MyCFG.node
-  ; control_context : Obj.t (** (Control.get_spec ()) context, represented type: unit -> (Control.get_spec ()).C.t *)
-  ; context  : unit -> 'c (** current Spec context *)
+  ; control_context : unit -> ControlSpecC.t (** top-level Control Spec context, raises [Ctx_failure] if missing *)
+  ; context  : unit -> 'c (** current Spec context, raises [Ctx_failure] if missing *)
   ; edge     : MyCFG.edge
   ; local    : 'd
   ; global   : 'v -> 'g

src/framework/constraints.ml

@@ -478,7 +478,7 @@ struct
       ; emit    = (fun _ -> failwith "emit outside MCP")
       ; node    = fst var
       ; prev_node = prev_node
-      ; control_context = snd var
+      ; control_context = snd var |> Obj.obj
       ; context = snd var |> Obj.obj
       ; edge    = edge
       ; local   = pval

src/framework/control.ml

@@ -31,6 +31,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
             |> lift (get_bool "ana.opt.hashcons") (module HashconsLifter)
           ) in
   GobConfig.building_spec := false;
+  Analyses.control_spec_c := (module S1.C);
   (module S1)
 )
 
@@ -261,7 +262,7 @@ struct
         ; emit   = (fun _ -> failwith "Cannot \"emit\" in global initializer context.")
         ; node    = MyCFG.dummy_node
         ; prev_node = MyCFG.dummy_node
-        ; control_context = Obj.repr (fun () -> ctx_failwith "Global initializers have no context.")
+        ; control_context = (fun () -> ctx_failwith "Global initializers have no context.")
         ; context = (fun () -> ctx_failwith "Global initializers have no context.")
         ; edge    = MyCFG.Skip
         ; local   = Spec.D.top ()
@@ -360,7 +361,7 @@ struct
         ; emit   = (fun _ -> failwith "Cannot \"emit\" in enter_with context.")
         ; node    = MyCFG.dummy_node
         ; prev_node = MyCFG.dummy_node
-        ; control_context = Obj.repr (fun () -> ctx_failwith "enter_func has no context.")
+        ; control_context = (fun () -> ctx_failwith "enter_func has no context.")
         ; context = (fun () -> ctx_failwith "enter_func has no context.")
         ; edge    = MyCFG.Skip
         ; local   = st
@@ -392,7 +393,7 @@ struct
         ; emit   = (fun _ -> failwith "Cannot \"emit\" in otherstate context.")
         ; node    = MyCFG.dummy_node
         ; prev_node = MyCFG.dummy_node
-        ; control_context = Obj.repr (fun () -> ctx_failwith "enter_func has no context.")
+        ; control_context = (fun () -> ctx_failwith "enter_func has no context.")
         ; context = (fun () -> ctx_failwith "enter_func has no context.")
         ; edge    = MyCFG.Skip
         ; local   = st
@@ -592,7 +593,7 @@ struct
                 ; emit   = (fun _ -> failwith "Cannot \"emit\" in query context.")
                 ; node   = MyCFG.dummy_node (* TODO maybe ask should take a node (which could be used here) instead of a location *)
                 ; prev_node = MyCFG.dummy_node
-                ; control_context = Obj.repr (fun () -> ctx_failwith "No context in query context.")
+                ; control_context = (fun () -> ctx_failwith "No context in query context.")
                 ; context = (fun () -> ctx_failwith "No context in query context.")
                 ; edge    = MyCFG.Skip
                 ; local  = local
@@ -645,7 +646,7 @@ struct
         ; emit   = (fun _ -> failwith "Cannot \"emit\" in query context.")
         ; node   = MyCFG.dummy_node (* TODO maybe ask should take a node (which could be used here) instead of a location *)
         ; prev_node = MyCFG.dummy_node
-        ; control_context = Obj.repr (fun () -> ctx_failwith "No context in query context.")
+        ; control_context = (fun () -> ctx_failwith "No context in query context.")
         ; context = (fun () -> ctx_failwith "No context in query context.")
         ; edge    = MyCFG.Skip
         ; local  = snd (List.hd startvars) (* bot and top both silently raise and catch Deadcode in DeadcodeLifter *)

src/witness/witness.ml

@@ -290,7 +290,7 @@ struct
         ; emit   = (fun _ -> failwith "Cannot \"emit\" in witness context.")
         ; node   = fst lvar
         ; prev_node = MyCFG.dummy_node
-        ; control_context = Obj.repr (fun () -> snd lvar)
+        ; control_context = (fun () -> Obj.magic (snd lvar)) (* magic is fine because Spec is top-level Control Spec *)
         ; context = (fun () -> snd lvar)
         ; edge    = MyCFG.Skip
         ; local  = local

src/witness/yamlWitness.ml

@@ -137,7 +137,7 @@ struct
         ; emit   = (fun _ -> failwith "Cannot \"emit\" in witness context.")
         ; node   = n
         ; prev_node = MyCFG.dummy_node
-        ; control_context = Obj.repr (fun () -> ctx_failwith "No context in witness context.")
+        ; control_context = (fun () -> ctx_failwith "No context in witness context.")
         ; context = (fun () -> ctx_failwith "No context in witness context.")
         ; edge    = MyCFG.Skip
         ; local  = local
@@ -239,7 +239,7 @@ struct
         ; emit   = (fun _ -> failwith "Cannot \"emit\" in witness context.")
         ; node   = fst lvar
         ; prev_node = MyCFG.dummy_node
-        ; control_context = Obj.repr (fun () -> snd lvar)
+        ; control_context = (fun () -> Obj.magic (snd lvar)) (* magic is fine because Spec is top-level Control Spec *)
         ; context = (fun () -> snd lvar)
         ; edge    = MyCFG.Skip
         ; local  = local