Replace ctx.assign with Assign event

Author: sim642

src/analyses/arinc.ml

@@ -337,7 +337,7 @@ struct
       let assign_id exp id =
         match exp with
         (* call assign for all analyses (we only need base)! *)
-        | AddrOf lval -> ctx.assign ~name:"base" lval (mkAddrOf @@ var id)
+        | AddrOf lval -> ctx.emit (Assign {lval; exp = mkAddrOf @@ var id})
         (* TODO not needed for the given code, but we could use Queries.MayPointTo exp in this case *)
         | _ -> failwith @@ "Could not assign id. Expected &id. Found "^sprint d_exp exp
       in

src/analyses/extract_arinc.ml

@@ -272,7 +272,7 @@ struct
         let assign_id exp id =
           if M.tracing then M.trace "extract_arinc" "assign_id %a %s\n" d_exp exp id.vname;
           match exp with
-          | AddrOf lval -> ctx.assign ~name:"base" lval (mkAddrOf @@ var id)
+          | AddrOf lval -> ctx.emit (Assign {lval; exp = mkAddrOf @@ var id})
           | _ -> failwith @@ "Could not assign id. Expected &id. Found "^sprint d_exp exp
         in
         (* evaluates an argument and returns a list of possible values for that argument. *)

src/analyses/extract_osek.ml

@@ -265,7 +265,7 @@ struct
         let assign_id exp id =
           if M.tracing then M.trace "extract_osek" "assign_id %a %s\n" d_exp exp id.vname;
           match exp with
-          | AddrOf lval -> ctx.assign ~name:"base" lval (mkAddrOf @@ var id)
+          | AddrOf lval -> ctx.emit (Assign {lval; exp = mkAddrOf @@ var id})
           | _ -> failwith @@ "Could not assign id. Expected &id. Found "^sprint d_exp exp
         in
         (* evaluates an argument and returns a list of possible values for that argument. *)

src/analyses/mCP.ml

@@ -113,6 +113,7 @@ struct
       ) x
 
   let should_join x y =
+    (* TODO: GobList.for_all3 *)
     let rec zip3 lst1 lst2 lst3 = match lst1,lst2,lst3 with
       | [],_, _ -> []
       | _,[], _ -> []
@@ -175,26 +176,6 @@ struct
     in
     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 *)
-    else
-      let spec_assign n d : Obj.t =
-        (* spec of current analysis *)
-        let (module S:MCPSpec) = spec n in
-        let assign_one d (lval, exp, name, ctx) =
-          match name with
-          | Some x when x <> find_spec_name n -> obj d (* do nothing if current spec name is filtered out *)
-          | _ ->
-            let ctx' = {(obj ctx) with local = obj d} in
-            S.assign ctx' lval exp
-        in
-        let get_lval (lval, exp, name, ctx) = lval in
-        (* group by assigns on the same lval -> only those must be joined *)
-        List.group (compareBy get_lval) assigns
-        |> List.fold_left (fun d xs -> List.map (assign_one d) xs |> List.reduce S.D.join |> repr) d
-      in
-      List.map (fun (n,d) -> n, spec_assign n d) xs
-
   let rec do_splits ctx pv (xs:(int * (Obj.t * Events.t list)) list) =
     let split_one n (d,emits) =
       let nv = assoc_replace (n,d) pv in
@@ -218,25 +199,25 @@ struct
     let do_emit ctx = function
       | Events.SplitBranch (exp, tv) ->
         ctx_with_local ctx (branch ctx exp tv)
+      | Events.Assign {lval; exp} ->
+        ctx_with_local ctx (assign ctx lval exp)
       | e ->
         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 ctx'' = outer_ctx "do_emits" ~spawns ~sides ~emits ctx in
         let octx'' = outer_ctx "do_emits" ~spawns ~sides ~emits octx in
         let f post_all (n,(module S:MCPSpec),(d,od)) =
-          let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "do_emits" ~splits ~assigns ~post_all ctx'' n d in
-          let octx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "do_emits" ~splits ~assigns ~post_all octx'' n d in
+          let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "do_emits" ~splits ~post_all ctx'' n d in
+          let octx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "do_emits" ~splits ~post_all octx'' n d in
           n, repr @@ S.event ctx' e octx'
         in
         let d, q = map_deadcode f @@ spec_list2 ctx.local octx.local in
         if M.tracing then M.tracel "event" "%a\n  before: %a\n  after:%a\n" Events.pretty e D.pretty ctx.local D.pretty d;
         do_sideg ctx !sides;
         do_spawns ctx !spawns;
         do_splits ctx d !splits;
-        let d = do_assigns ctx !assigns d in
         let d = do_emits ctx !emits d in
         if q then raise Deadcode else ctx_with_local ctx d
     in
@@ -247,18 +228,16 @@ struct
     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 ctx'' = outer_ctx "branch" ~spawns ~sides ~emits ctx in
     let f post_all (n,(module S:MCPSpec),d) =
-      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "branch" ~splits ~assigns ~post_all ctx'' n d in
+      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "branch" ~splits ~post_all ctx'' n d in
       n, repr @@ S.branch ctx' e tv
     in
     let d, q = map_deadcode f @@ spec_list ctx.local in
     do_sideg ctx !sides;
     do_spawns ctx !spawns;
     do_splits ctx d !splits;
-    let d = do_assigns ctx !assigns d in
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
@@ -343,7 +322,7 @@ struct
     }
 
   (* Explicitly polymorphic type required here for recursive call in branch. *)
-  and inner_ctx: type d g c v. string -> ?splits:(int * (Obj.t * Events.t list)) list ref -> ?assigns:(lval * exp * string option * Obj.t) list ref -> ?post_all:(int * Obj.t) list -> (D.t, G.t, C.t, V.t) ctx -> int -> Obj.t -> (d, g, c, v) ctx = fun tfname ?splits ?assigns ?(post_all=[]) ctx n d ->
+  and inner_ctx: type d g c v. string -> ?splits:(int * (Obj.t * Events.t list)) list ref -> ?post_all:(int * Obj.t) list -> (D.t, G.t, C.t, V.t) ctx -> int -> Obj.t -> (d, g, c, v) ctx = fun tfname ?splits ?(post_all=[]) ctx n d ->
     let split = match splits with
       | Some splits -> (fun d es   -> splits := (n,(repr d,es)) :: !splits)
       | None -> (fun _ _    -> failwith ("Cannot \"split\" in " ^ tfname ^ " context."))
@@ -356,16 +335,11 @@ struct
       ; global = (fun v      -> ctx.global (v_of n v) |> g_to n |> obj)
       ; split
       ; sideg  = (fun v g    -> ctx.sideg (v_of n v) (`Lifted (n, repr g)))
-      ; assign = (
-        match assigns with
-        | Some assigns -> (fun ?name v e -> assigns := (v,e,name, repr ctx')::!assigns)
-        | None -> (fun ?name _ -> failwith ("Cannot \"assign\" in " ^ tfname ^ " context."))
-      )
       }
     in
     ctx'
 
-  let assign (ctx:(D.t, G.t, C.t, V.t) ctx) l e =
+  and 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
@@ -404,113 +378,101 @@ struct
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in
-    let assigns = ref [] in
     let emits = ref [] in
     let ctx'' = outer_ctx "body" ~spawns ~sides ~emits ctx in
     let f post_all (n,(module S:MCPSpec),d) =
-      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "body" ~splits ~assigns ~post_all ctx'' n d in
+      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "body" ~splits ~post_all ctx'' n d in
       n, repr @@ S.body ctx' f
     in
     let d, q = map_deadcode f @@ spec_list ctx.local in
     do_sideg ctx !sides;
     do_spawns ctx !spawns;
     do_splits ctx d !splits;
-    let d = do_assigns ctx !assigns d in
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
   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 ctx'' = outer_ctx "return" ~spawns ~sides ~emits ctx in
     let f post_all (n,(module S:MCPSpec),d) =
-      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "return" ~splits ~assigns ~post_all ctx'' n d in
+      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "return" ~splits ~post_all ctx'' n d in
       n, repr @@ S.return ctx' e f
     in
     let d, q = map_deadcode f @@ spec_list ctx.local in
     do_sideg ctx !sides;
     do_spawns ctx !spawns;
     do_splits ctx d !splits;
-    let d = do_assigns ctx !assigns d in
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
   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 ctx'' = outer_ctx "interpt" ~spawns ~sides ~emits ctx in
     let f post_all (n,(module S:MCPSpec),d) =
-      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "interpt" ~splits ~assigns ~post_all ctx'' n d in
+      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "interpt" ~splits ~post_all ctx'' n d in
       n, repr @@ S.intrpt ctx'
     in
     let d, q = map_deadcode f @@ spec_list ctx.local in
     do_sideg ctx !sides;
     do_spawns ctx !spawns;
     do_splits ctx d !splits;
-    let d = do_assigns ctx !assigns d in
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
   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 ctx'' = outer_ctx "asm" ~spawns ~sides ~emits ctx in
     let f post_all (n,(module S:MCPSpec),d) =
-      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "asm" ~splits ~assigns ~post_all ctx'' n d in
+      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "asm" ~splits ~post_all ctx'' n d in
       n, repr @@ S.asm ctx'
     in
     let d, q = map_deadcode f @@ spec_list ctx.local in
     do_sideg ctx !sides;
     do_spawns ctx !spawns;
     do_splits ctx d !splits;
-    let d = do_assigns ctx !assigns d in
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
   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 ctx'' = outer_ctx "skip" ~spawns ~sides ~emits ctx in
     let f post_all (n,(module S:MCPSpec),d) =
-      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "skip" ~splits ~assigns ~post_all ctx'' n d in
+      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "skip" ~splits ~post_all ctx'' n d in
       n, repr @@ S.skip ctx'
     in
     let d, q = map_deadcode f @@ spec_list ctx.local in
     do_sideg ctx !sides;
     do_spawns ctx !spawns;
     do_splits ctx d !splits;
-    let d = do_assigns ctx !assigns d in
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
   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 ctx'' = outer_ctx "special" ~spawns ~sides ~emits ctx in
     let f post_all (n,(module S:MCPSpec),d) =
-      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "special" ~splits ~assigns ~post_all ctx'' n d in
+      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "special" ~splits ~post_all ctx'' n d in
       n, repr @@ S.special ctx' r f a
     in
     let d, q = map_deadcode f @@ spec_list ctx.local in
     do_sideg ctx !sides;
     do_spawns ctx !spawns;
     do_splits ctx d !splits;
-    let d = do_assigns ctx !assigns d in
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 
@@ -547,7 +509,6 @@ struct
   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 ctx'' = outer_ctx "combine" ~spawns ~sides ~emits ctx in
     (* Like spec_list2 but for three lists. Tail recursion like map3_rev would have.
@@ -565,13 +526,12 @@ struct
       | _, _, _ -> invalid_arg "MCP.spec_list3_rev_acc"
     in
     let f post_all (n,(module S:MCPSpec),(d,fc,fd)) =
-      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "combine" ~assigns ~post_all ctx'' n d in
+      let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "combine" ~post_all ctx'' n d in
       n, repr @@ S.combine ctx' r fe f a (Option.map obj fc) (obj fd)
     in
     let d, q = map_deadcode f @@ List.rev @@ spec_list3_rev_acc [] ctx.local fc fd in
     do_sideg ctx !sides;
     do_spawns ctx !spawns;
-    let d = do_assigns ctx !assigns d in
     let d = do_emits ctx !emits d in
     if q then raise Deadcode else d
 

src/domains/events.ml

@@ -8,6 +8,7 @@ type t =
   | SplitBranch of exp * bool (** Used to simulate old branch-based split. *)
   | AssignSpawnedThread of lval * ThreadIdDomain.Thread.t (** Assign spawned thread's ID to lval. *)
   | Access of {var_opt: CilType.Varinfo.t option; write: bool} (** Access varinfo (unknown if None). *)
+  | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [ctx.assign]. *)
 
 let pretty () = function
   | Lock m -> dprintf "Lock %a" LockDomain.Addr.pretty m
@@ -17,3 +18,4 @@ let pretty () = function
   | SplitBranch (exp, tv) -> dprintf "SplitBranch (%a, %B)" d_exp exp tv
   | AssignSpawnedThread (lval, tid) -> dprintf "AssignSpawnedThread (%a, %a)" d_lval lval ThreadIdDomain.Thread.pretty tid
   | Access {var_opt; write} -> dprintf "Access {var_opt=%a, write=%B}" (docOpt (CilType.Varinfo.pretty ())) var_opt write
+  | Assign {lval; exp} -> dprintf "Assugn {lval=%a, exp=%a}" CilType.Lval.pretty lval CilType.Exp.pretty exp

src/framework/analyses.ml

@@ -315,7 +315,6 @@ type ('d,'g,'c,'v) ctx =
   ; spawn    : lval option -> varinfo -> exp list -> unit
   ; split    : 'd -> Events.t list -> unit
   ; sideg    : 'v -> 'g -> unit
-  ; assign   : ?name:string -> lval -> exp -> unit
   }
 
 exception Ctx_failure of string

src/framework/constraints.ml

@@ -498,7 +498,6 @@ struct
       ; spawn   = spawn
       ; split   = (fun (d:D.t) es -> assert (List.is_empty es); r := d::!r)
       ; sideg   = sideg
-      ; assign = (fun ?name _    -> failwith "Cannot \"assign\" in common context.")
       }
     and spawn lval f args =
       (* TODO: adjust ctx node/edge? *)

src/framework/control.ml

@@ -250,7 +250,6 @@ struct
         ; spawn   = (fun _ -> failwith "Global initializers should never spawn threads. What is going on?")
         ; split   = (fun _ -> failwith "Global initializers trying to split paths.")
         ; sideg   = sideg
-        ; assign  = (fun ?name _ -> failwith "Global initializers trying to assign.")
         }
       in
       let edges = CfgTools.getGlobalInits file in
@@ -348,7 +347,6 @@ struct
         ; spawn   = (fun _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
         ; split   = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.")
         ; sideg   = sideg
-        ; assign  = (fun ?name _ -> failwith "Bug4: Using enter_func for toplevel functions with 'otherstate'.")
         }
       in
       let args = List.map (fun x -> MyCFG.unknown_exp) fd.sformals in
@@ -383,7 +381,6 @@ struct
         ; spawn   = (fun _ -> failwith "Bug1: Using enter_func for toplevel functions with 'otherstate'.")
         ; split   = (fun _ -> failwith "Bug2: Using enter_func for toplevel functions with 'otherstate'.")
         ; sideg   = sideg
-        ; assign  = (fun ?name _ -> failwith "Bug4: Using enter_func for toplevel functions with 'otherstate'.")
         }
       in
       (* TODO: don't hd *)
@@ -574,7 +571,6 @@ struct
             ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in query context.")
             ; split  = (fun d es   -> failwith "Cannot \"split\" in query context.")
             ; sideg  = (fun v g    -> failwith "Cannot \"split\" in query context.")
-            ; assign = (fun ?name _ -> failwith "Cannot \"assign\" in query context.")
             }
           in
           Spec.query ctx
@@ -629,7 +625,6 @@ struct
         ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in query context.")
         ; split  = (fun d es   -> failwith "Cannot \"split\" in query context.")
         ; sideg  = (fun v g    -> failwith "Cannot \"split\" in query context.")
-        ; assign = (fun ?name _ -> failwith "Cannot \"assign\" in query context.")
         }
       in
       Spec.query ctx (WarnGlobal (Obj.repr g))

src/witness/witness.ml

@@ -309,7 +309,6 @@ struct
         ; spawn  = (fun v d    -> failwith "Cannot \"spawn\" in witness context.")
         ; split  = (fun d es   -> failwith "Cannot \"split\" in witness context.")
         ; sideg  = (fun v g    -> failwith "Cannot \"sideg\" in witness context.")
-        ; assign = (fun ?name _ -> failwith "Cannot \"assign\" in witness context.")
         }
       in
       Spec.query ctx