todo: starting at valueDomain.ml (email), wtf should I do in cfgtools

Author: Simon Tietz

src/analyses/accessAnalysis.ml

@@ -25,10 +25,9 @@ struct
 
   let collect_local = ref false
   let emit_single_threaded = ref false
-  let ignore_asm = ref true
+  let ignore_asm = get_bool "asm_is_nop"
 
   let init _ =
-    ignore_asm := get_bool "asm_is_nop";
     collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed";
     let activated = get_string_list "ana.activated" in
     emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
@@ -76,11 +75,12 @@ struct
     end
 
   let asm ctx =
-    if not !ignore_asm then begin
+    if not ignore_asm then begin
       let ins, outs = Analyses.asm_extract_ins_outs ctx in
       let handle_in exp = access_one_top ctx Read false exp in
       List.iter handle_in ins;
-      let handle_out lval = access_one_top ctx Write false (AddrOf lval) in
+      (* deref needs to be set to true because we have to use AddrOf *)
+      let handle_out lval = access_one_top ~deref:true ctx Write false (AddrOf lval) in
       List.iter handle_out outs;
     end;
     ctx.local

src/analyses/base.ml

@@ -2889,9 +2889,13 @@ struct
     in
     D.join ctx.local e_d'
 
+  let ignore_asm = get_bool "asm_is_nop"
+
   let asm ctx = 
-    let _, outs = Analyses.asm_extract_ins_outs ctx in
-    ctx.emit (Events.Invalidate {lvals=outs});
+    if not ignore_asm then begin
+      let _, outs = Analyses.asm_extract_ins_outs ctx in
+      ctx.emit (Events.Invalidate {lvals=outs});
+    end;
     ctx.local
 
   let event ctx e octx =

src/analyses/malloc_null.ml

@@ -17,11 +17,7 @@ struct
   module C = ValueDomain.AddrSetDomain
   module P = IdentityP (D)
 
-  let ignore_asm = ref true
-
-  (*TODO: why is this init not called??? *)
-  let init _ =
-    ignore_asm := get_bool "asm_is_nop"
+  let ignore_asm = get_bool "asm_is_nop"
 
   (*
     Addr set functions:
@@ -161,9 +157,7 @@ struct
     | _ -> ctx.local
 
   let asm ctx =
-    (* tmp hack because init is broken *)
-    let ignore_asm = ref (get_bool "asm_is_nop") in
-    if not !ignore_asm then begin
+    if not ignore_asm then begin
       let ins, outs = Analyses.asm_extract_ins_outs ctx in
       let handle_in exp = warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local exp in
       List.iter handle_in ins;

src/analyses/modifiedSinceSetjmp.ml

@@ -67,14 +67,6 @@ struct
     match e with
     | Access {ad; kind = Write; _} ->
       add_to_all_defined (relevants_from_ad ad) ctx.local
-    | Invalidate {lvals} ->
-      let lval_to_vs lval = 
-        let e = AddrOf lval in
-        let mpt: _ Queries.t = MayPointTo e in 
-        let ad = ctx.ask mpt in
-        relevants_from_ad ad in
-      let vss = List.map lval_to_vs lvals in
-      List.fold_left (fun d vs -> add_to_all_defined vs d) ctx.local vss
     | _ ->
       ctx.local
 end

src/analyses/uninit.ml

@@ -30,10 +30,7 @@ struct
   let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v : D.t = D.empty ()
 
-  let ignore_asm = ref true
-
-  let init _ = 
-    ignore_asm := get_bool "asm_is_nop"
+  let ignore_asm = get_bool "asm_is_nop"
 
   let access_address (ask: Queries.ask) write lv =
     match ask.f (Queries.MayPointTo (AddrOf lv)) with
@@ -230,11 +227,13 @@ struct
     init_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
   let asm ctx = 
-    let ins, outs = Analyses.asm_extract_ins_outs ctx in
-    let handle_in exp = ignore (is_expr_initd (Analyses.ask_of_ctx ctx) exp ctx.local) in
-    List.iter handle_in ins;
-    let handle_out local lval = init_lval (Analyses.ask_of_ctx ctx) lval local in
-    List.fold_left handle_out ctx.local outs
+    if not ignore_asm then begin
+      let ins, outs = Analyses.asm_extract_ins_outs ctx in
+      let handle_in exp = ignore (is_expr_initd (Analyses.ask_of_ctx ctx) exp ctx.local) in
+      List.iter handle_in ins;
+      let handle_out local lval = init_lval (Analyses.ask_of_ctx ctx) lval local in
+      List.fold_left handle_out ctx.local outs
+    end else ctx.local
 
   let branch ctx (exp:exp) (tv:bool) : trans_out =
     ignore (is_expr_initd (Analyses.ask_of_ctx ctx) exp ctx.local);

src/analyses/useAfterFree.ml

@@ -25,10 +25,7 @@ struct
   module G = ThreadIdToJoinedThreadsMap
   module V = VarinfoV
 
-  let ignore_asm = ref true
-
-  let init _ =
-    ignore_asm := get_bool "asm_is_nop"
+  let ignore_asm = get_bool "asm_is_nop"
 
   let context _ _ = ()
   (* HELPER FUNCTIONS *)
@@ -176,7 +173,7 @@ struct
     ctx.local
 
   let asm ctx =
-    if not !ignore_asm then begin
+    if not ignore_asm then begin
       let ins, outs = Analyses.asm_extract_ins_outs ctx in
       let handle_out lval = warn_lval_might_contain_freed "asm" ctx lval in
       List.iter handle_out outs;

src/common/framework/cfgTools.ml

@@ -141,8 +141,6 @@ end
 
 module CfgEdgeH = BatHashtbl.Make (CfgEdge)
 
-let ignore_asm = get_bool "asm_is_nop"
-
 let createCFG (file: file) =
   let cfgF = H.create 113 in
   let cfgB = H.create 113 in
@@ -378,19 +376,21 @@ let createCFG (file: file) =
 
           | Asm (_, tmpls, outs, ins, _, labels, loc) ->
             begin match real_succs () with
-            | [] -> failwith "MyCFG.createCFG: 0 Asm succ"
-            | [succ, skippedStatements] -> begin
+              | [] -> failwith "MyCFG.createCFG: 0 Asm succ"
+              | [succ, skippedStatements] -> begin
                 addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, false)) (Statement succ);
-                if not ignore_asm then
-                  List.iter (fun label ->
-                      let succ, skippedStatements = find_real_stmt ~parent:stmt !label in 
-                      addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, true)) (Statement succ)
-                    ) labels
-                else ()
+                let unique_dests = List.fold_left (fun acc label ->
+                  let succ, skippedStatements = find_real_stmt ~parent:stmt !label in
+                  match List.assoc_opt succ acc with
+                  | Some _ -> acc
+                  | None -> (succ, skippedStatements) :: acc
+                ) [] labels in
+                List.iter (fun (succ, skippedStatements) ->
+                  addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, true)) (Statement succ)
+                ) unique_dests;
               end
-            | _ -> failwith "MyCFG.createCFG: >1 Asm succ"
+              | _ -> failwith "MyCFG.createCFG: >1 Asm succ"
             end
-
           | Continue _
           | Break _
           | Switch _ ->