[exit_points] generic env + catch Not_found when searching in env

src/plugins/e-acsl/exit_points.ml

@@ -23,6 +23,28 @@
 open Cil_types
 open Cil_datatype
 
+module Build_env(X: sig type t val name: string end): sig
+  val add: stmt -> X.t -> unit
+  val get: stmt -> X.t
+  val get_all: stmt -> X.t list
+  val is_empty: unit -> bool
+  val clear: unit -> unit
+end = struct
+
+  let tbl = Stmt.Hashtbl.create 17
+  let add = Stmt.Hashtbl.add tbl
+
+  let get stmt =
+    try Stmt.Hashtbl.find tbl stmt
+    with Not_found ->
+      Options.fatal "unknown stmt %a in %s" Printer.pp_stmt stmt X.name
+
+  let get_all = Stmt.Hashtbl.find_all tbl
+  let is_empty () = Stmt.Hashtbl.length tbl = 0
+  let clear () = Stmt.Hashtbl.clear tbl
+
+end
+
 (* Mapping of statements to local variables available within that statement's
    scope. The mappings of this structure are used to determine variables which
    need to be removed before goto jumps. Generally, if some goto (with
@@ -30,21 +52,8 @@ open Cil_datatype
    scope variables given by set L', then the goto exists the scopes of
    variables given via set G' \ L'. Consequently, if those variables are
    tracked, they need to be removed from tracking. *)
-module SLocals: sig
-  val add: stmt -> varinfo list -> unit
-  val find: stmt -> Varinfo.Set.t
-  val is_empty: unit -> bool
-  val reset: unit -> unit
-end = struct
-  let statement_locals = Stmt.Hashtbl.create 17
-  let add stmt locals =
-    Stmt.Hashtbl.replace statement_locals stmt (Varinfo.Set.of_list locals)
-  let find stmt =
-    Stmt.Hashtbl.find statement_locals stmt
-  let is_empty () =
-    Stmt.Hashtbl.length statement_locals = 0
-  let reset () = Stmt.Hashtbl.reset statement_locals
-end
+module SLocals =
+  Build_env(struct type t = Varinfo.Set.t let name = "SLocals" end)
 
 (* Statement to statement mapping indicating source/destination of a jump.
    For instance, break statements are mapped to switches or loops they jump
@@ -52,43 +61,17 @@ end
    such information does not really be computed for gotos (since they already
    capture references to labelled statements they jumps to). Nevertheless it is
    done for consistency, so all required information is stored uniformly. *)
-module Exits: sig
-  val add: stmt -> stmt -> unit
-  val find: stmt -> stmt
-  val is_empty: unit -> bool
-  val reset: unit -> unit
-end = struct
-  let exit_context = Stmt.Hashtbl.create 17
-  let add stmt from =
-    Stmt.Hashtbl.replace exit_context stmt from
-  let find stmt =
-    Stmt.Hashtbl.find exit_context stmt
-  let is_empty () =
-    Stmt.Hashtbl.length exit_context = 0
-  let reset () = Stmt.Hashtbl.reset exit_context
-end
+module Exits =
+  Build_env(struct type t = stmt let name = "Exits" end)
 
 (* Map labelled statements back to gotos which lead to them *)
-module LJumps: sig
-  val add: stmt -> stmt -> unit
-  val find_all: stmt -> stmt list
-  val is_empty: unit -> bool
-  val reset: unit -> unit
-end = struct
-  let labelled_jumps = Stmt.Hashtbl.create 17
-  let find_all stmt =
-    Stmt.Hashtbl.find_all labelled_jumps stmt
-  let add label goto =
-    Stmt.Hashtbl.add labelled_jumps label goto
-  let is_empty () =
-    Stmt.Hashtbl.length labelled_jumps = 0
-  let reset () = Stmt.Hashtbl.reset labelled_jumps
-end
+module LJumps =
+  Build_env(struct type t = stmt let name = "LJumps" end)
 
-let reset () =
-  SLocals.reset ();
-  Exits.reset ();
-  LJumps.reset ()
+let clear () =
+  SLocals.clear ();
+  Exits.clear ();
+  LJumps.clear ()
 
 let is_empty () =
   SLocals.is_empty () && Exits.is_empty () && LJumps.is_empty ()
@@ -96,20 +79,25 @@ let is_empty () =
 let delete_vars stmt =
   match stmt.skind with
   | Goto _ | Break _ | Continue _ ->
-    Varinfo.Set.diff (SLocals.find stmt) (SLocals.find (Exits.find stmt))
+    Varinfo.Set.diff (SLocals.get stmt) (SLocals.get (Exits.get stmt))
   | _ ->
     Varinfo.Set.empty
 
 let store_vars stmt =
-  let gotos = LJumps.find_all stmt in
+  let gotos = LJumps.get_all stmt in
   List.fold_left
     (fun acc goto ->
       Varinfo.Set.union
         acc
-        (Varinfo.Set.diff (SLocals.find stmt) (SLocals.find goto)))
+        (Varinfo.Set.diff (SLocals.get stmt) (SLocals.get goto)))
     Varinfo.Set.empty
     gotos
 
+let list_flatten_to_set =
+  List.fold_left
+    (List.fold_left (fun acc v -> Varinfo.Set.add v acc))
+    Varinfo.Set.empty
+
 class jump_context = object (_)
   inherit Visitor.frama_c_inplace
 
@@ -128,24 +116,24 @@ class jump_context = object (_)
 
   method !vstmt stmt =
     match stmt.skind with
-    | Loop(_) | Switch(_) ->
-      SLocals.add stmt (List.flatten locals);
+    | Loop _ | Switch _ ->
+      SLocals.add stmt (list_flatten_to_set locals);
       Stack.push stmt jumps;
       Cil.DoChildrenPost (fun st -> ignore(Stack.pop jumps); st)
-    | Break(_) | Continue(_) ->
+    | Break _ | Continue _ ->
       Exits.add stmt (Stack.top jumps);
-      SLocals.add stmt (List.flatten locals);
+      SLocals.add stmt (list_flatten_to_set locals);
       Cil.DoChildren
     | Goto(sref, _)  ->
-      SLocals.add stmt (List.flatten locals);
+      SLocals.add stmt (list_flatten_to_set locals);
       Exits.add stmt !sref;
       LJumps.add !sref stmt;
       Cil.DoChildren
-    | Instr(_) | Return(_) | If(_) | Block(_) | UnspecifiedSequence(_)
-    | Throw(_) | TryCatch(_) | TryFinally(_) | TryExcept(_) ->
+    | Instr _ | Return _ | If _ | Block _ | UnspecifiedSequence _
+    | Throw _ | TryCatch _ | TryFinally _ | TryExcept _ ->
       (match stmt.labels with
       | [] -> ()
-      | _ :: _ -> SLocals.add stmt (List.flatten locals));
+      | _ :: _ -> SLocals.add stmt (list_flatten_to_set locals));
       Cil.DoChildren
 end
 

src/plugins/e-acsl/exit_points.mli

@@ -34,7 +34,7 @@ open Cil_datatype
 val generate: fundec -> unit
 (** Visit a function and populate data structures used to compute exit points *)
 
-val reset: unit -> unit
+val clear: unit -> unit
 (** Clear all gathered data *)
 
 val delete_vars: stmt -> Varinfo.Set.t

src/plugins/e-acsl/visit.ml

@@ -439,7 +439,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
       List.iter (fun vi -> vi.vghost <- false) f.slocals;
       Cil.DoChildrenPost
         (fun f ->
-          Exit_points.reset ();
+          Exit_points.clear ();
           self#add_generated_variables_in_function f;
           Options.feedback ~dkey ~level:2 "function %a done."
             Kernel_function.pretty kf;