From ecda9943f539d007ba5d36343a03840b912890e2 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Fri, 17 Nov 2023 17:09:12 +0100
Subject: [PATCH 01/62] test

---
 src/common/util/cilfacade.ml  | 3 ++-
 src/common/util/cilfacade0.ml | 2 +-
 src/maingoblint.ml            | 2 ++
 3 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index ba57074e5a..9dc68dd5fc 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -483,13 +483,14 @@ class countFnVisitor = object
     | Switch (_,_,_,loc,_)
     | Loop (_,loc,_,_,_)
       -> Hashtbl.replace locs loc.line (); DoChildren
+    | Asm (_,_,_,_,_,_,loc)
+      -> Hashtbl.replace locs loc.line (); SkipChildren
     | _ ->
       DoChildren
 
   method! vinst = function
     | Set (_,_,loc,_)
     | Call (_,_,_,loc,_)
-    | Asm (_,_,_,_,_,loc)
       -> Hashtbl.replace locs loc.line (); SkipChildren
     | _ -> SkipChildren
 
diff --git a/src/common/util/cilfacade0.ml b/src/common/util/cilfacade0.ml
index 35fd5fb706..989d0bd316 100644
--- a/src/common/util/cilfacade0.ml
+++ b/src/common/util/cilfacade0.ml
@@ -29,7 +29,6 @@ let eloc_fallback ~eloc ~loc =
 let get_instrLoc = function
   | Set (_, _, loc, eloc) -> eloc_fallback ~eloc ~loc
   | Call (_, _, _, loc, eloc) -> eloc_fallback ~eloc ~loc
-  | Asm (_, _, _, _, _, loc) -> loc
   | VarDecl (_, loc) -> loc
 
 (** Get expression location for [Cil.stmt]. *)
@@ -51,3 +50,4 @@ let rec get_stmtLoc stmt =
   | Switch (_, _, _, loc, eloc) -> eloc_fallback ~eloc ~loc
   | Loop (_, loc, eloc, _, _) -> eloc_fallback ~eloc ~loc
   | Block {bstmts = hd :: _; _} -> get_stmtLoc hd
+  | Asm (_, _, _, _, _, _, loc) -> loc
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index b5998df2d1..d55eaf1c4f 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -455,6 +455,8 @@ let parse_preprocessed preprocessed =
       Cilfacade.getAST preprocessed_file
     with
     | Frontc.ParseError s ->
+      if !E.hadErrors then
+        E.s (E.error "There were parsing errors in %s" fileName_str);
       raise (FrontendError (Format.sprintf "Frontc.ParseError: %s" s))
     | Errormsg.Error ->
       raise (FrontendError "Errormsg.Error")

From 33a853939ba00586c0bb8f09845499a76c5223ef Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Wed, 22 Nov 2023 09:48:24 +0100
Subject: [PATCH 02/62] tiny commit so someone else doesn't have to fix
 compareAST

---
 src/framework/cfgTools.ml     |  9 +++++++--
 src/incremental/compareAST.ml | 11 ++++++-----
 2 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
index 8f98a48e84..f9052d48e6 100644
--- a/src/framework/cfgTools.ml
+++ b/src/framework/cfgTools.ml
@@ -217,7 +217,8 @@ let createCFG (file: file) =
 
         | Instr _
         | If _
-        | Return _ ->
+        | Return _
+        | Asm _ ->
           stmt, visited_stmts
 
         | Continue _
@@ -295,7 +296,6 @@ let createCFG (file: file) =
             let edge_of_instr = function
               | Set (lval,exp,loc,eloc) -> Cilfacade.eloc_fallback ~eloc ~loc, Assign (lval, exp)
               | Call (lval,func,args,loc,eloc) -> Cilfacade.eloc_fallback ~eloc ~loc, Proc (lval,func,args)
-              | Asm (attr,tmpl,out,inp,regs,loc) -> loc, ASM (tmpl,out,inp)
               | VarDecl (v, loc) -> loc, VDecl(v)
             in
             let edges = List.map edge_of_instr instrs in
@@ -378,6 +378,10 @@ let createCFG (file: file) =
             (* Nothing to do, find_real_stmt skips over these. *)
             ()
 
+          | Asm (_, _, _, _, _, labels, _) ->
+              (* todo: how to do the duplication??? *)
+              ()
+
           | Continue _
           | Break _
           | Switch _ ->
@@ -386,6 +390,7 @@ let createCFG (file: file) =
 
           | ComputedGoto _ ->
             failwith "CfgTools.createCFG: unsupported stmt"
+        
         in
         Timing.wrap ~args:[("function", `String fd.svar.vname)] "handle" (List.iter handle) fd.sallstmts;
 
diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
index c79735c2b1..e73e64a029 100644
--- a/src/incremental/compareAST.ml
+++ b/src/incremental/compareAST.ml
@@ -309,11 +309,6 @@ let eq_instr (a: instr) (b: instr) ~(rename_mapping: rename_mapping) = match a,
     eq_lval lv1 lv2 ~rename_mapping &&>> eq_exp f1 f2 &&>> forward_list_equal eq_exp args1 args2
   | Call (None, f1, args1, _l1, _el1), Call (None, f2, args2, _l2, _el2) ->
     eq_exp f1 f2 ~rename_mapping &&>> forward_list_equal eq_exp args1 args2
-  | Asm (attr1, tmp1, ci1, dj1, rk1, l1), Asm (attr2, tmp2, ci2, dj2, rk2, l2) ->
-    (GobList.equal String.equal tmp1 tmp2, rename_mapping) &&>>
-    forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_lval z1 z2) ci1 ci2 &&>>
-    forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_exp z1 z2) dj1 dj2 &&>
-    GobList.equal String.equal rk1 rk2(* ignore attributes and locations *)
   | VarDecl (v1, _l1), VarDecl (v2, _l2) -> eq_varinfo v1 v2 ~rename_mapping
   | _, _ -> false, rename_mapping
 
@@ -351,6 +346,12 @@ let rec eq_stmtkind ?(cfg_comp = false) ((a, af): stmtkind * fundec) ((b, bf): s
   | Switch (exp1, block1, stmts1, _l1, _el1), Switch (exp2, block2, stmts2, _l2, _el2) -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else eq_exp exp1 exp2 ~rename_mapping &&>> eq_block' block1 block2 &&>> forward_list_equal (fun a b -> eq_stmt (a,af) (b,bf)) stmts1 stmts2
   | Loop (block1, _l1, _el1, _con1, _br1), Loop (block2, _l2, _el2, _con2, _br2) -> eq_block' block1 block2 ~rename_mapping
   | Block block1, Block block2 -> eq_block' block1 block2 ~rename_mapping
+  | Asm (attr1, tmp1, ci1, dj1, rk1, lb1, l1), Asm (attr2, tmp2, ci2, dj2, rk2, lb2, l2) ->
+    (GobList.equal String.equal tmp1 tmp2, rename_mapping) &&>>
+    forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_lval z1 z2) ci1 ci2 &&>>
+    forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_exp z1 z2) dj1 dj2 &&>
+    GobList.equal String.equal rk1 rk2(* ignore attributes and locations *) &&>
+    GobList.equal (fun st1 st2 -> eq_stmt_with_location (!st1, af) (!st2, bf)) lb1 lb2
   | _, _ -> false, rename_mapping
 
 and eq_stmt ?cfg_comp ((a, af): stmt * fundec) ((b, bf): stmt * fundec) ~(rename_mapping: rename_mapping) =

From 50901d1da4ff687615be20756c271c12adb2efbd Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Wed, 22 Nov 2023 16:16:07 +0100
Subject: [PATCH 03/62] cfg done; indentation complaints but I don't want to
 fix right now

---
 src/common/framework/edge.ml  |  8 ++++----
 src/common/framework/myCFG.ml |  2 +-
 src/framework/cfgTools.ml     | 15 ++++++++++++---
 src/framework/constraints.ml  |  2 +-
 src/goblint.ml                |  2 +-
 src/maingoblint.ml            |  7 ++++---
 src/transform/deadCode.ml     |  4 ++--
 7 files changed, 25 insertions(+), 15 deletions(-)

diff --git a/src/common/framework/edge.ml b/src/common/framework/edge.ml
index e6f214a4c8..fc918c80db 100644
--- a/src/common/framework/edge.ml
+++ b/src/common/framework/edge.ml
@@ -21,9 +21,9 @@ type t =
     * transferred to the function node! *)
   | Test of CilType.Exp.t * bool
   (** The true-branch or false-branch of a conditional exp *)
-  | ASM of string list * asm_out * asm_in
+  | ASM of string list * asm_out * asm_in * bool
   (** Inline assembly statements, and the annotations for output and input
-    * variables. *)
+    * variables. The last field is a flag that indicates if this is a duplicated edge. *)
   | VDecl of CilType.Varinfo.t
   (** VDecl edge for the variable in varinfo. Whether such an edge is there for all
     * local variables or only when it is not possible to pull the declaration up, is
@@ -43,7 +43,7 @@ let pretty () = function
   | Entry (f) -> Pretty.text "(body)"
   | Ret (Some e,f) -> Pretty.dprintf "return %a" dn_exp e
   | Ret (None,f) -> Pretty.dprintf "return"
-  | ASM (_,_,_) -> Pretty.text "ASM ..."
+  | ASM (_,_,_,_) -> Pretty.text "ASM ..."
   | Skip -> Pretty.text "skip"
   | VDecl v -> Cil.defaultCilPrinter#pVDecl () v
 
@@ -91,7 +91,7 @@ let to_yojson e =
         ("function", CilType.Fundec.to_yojson function_);
         ("exp", [%to_yojson: CilType.Exp.t option] exp);
       ]
-    | ASM (instructions, output, input) ->
+    | ASM (instructions, output, input, _) ->
       [
         ("type", `String "asm");
         ("instructions", [%to_yojson: string list] instructions);
diff --git a/src/common/framework/myCFG.ml b/src/common/framework/myCFG.ml
index 76675f3c88..5a66d220db 100644
--- a/src/common/framework/myCFG.ml
+++ b/src/common/framework/myCFG.ml
@@ -17,7 +17,7 @@ type edge = Edge.t =
   | Entry of CilType.Fundec.t
   | Ret of CilType.Exp.t option * CilType.Fundec.t
   | Test of CilType.Exp.t * bool
-  | ASM of string list * Edge.asm_out * Edge.asm_in
+  | ASM of string list * Edge.asm_out * Edge.asm_in * bool
   | VDecl of CilType.Varinfo.t
   | Skip
 
diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
index f9052d48e6..62b63570d3 100644
--- a/src/framework/cfgTools.ml
+++ b/src/framework/cfgTools.ml
@@ -378,9 +378,18 @@ let createCFG (file: file) =
             (* Nothing to do, find_real_stmt skips over these. *)
             ()
 
-          | Asm (_, _, _, _, _, labels, _) ->
-              (* todo: how to do the duplication??? *)
-              ()
+          | Asm (_, tmpls, outs, ins, _, labels, loc) ->
+            begin match real_succs () with
+            | [] -> failwith "MyCFG.createCFG: 0 Asm succ"
+            | [succ, skippedStatements] -> begin
+                addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, false)) (Statement succ);
+                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
+              end
+            | _ -> failwith "MyCFG.createCFG: >1 Asm succ"
+            end
 
           | Continue _
           | Break _
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 812d056de4..668ef0a3d7 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -807,7 +807,7 @@ struct
       | Entry f        -> tf_entry var edge prev_node f
       | Ret (r,fd)     -> tf_ret var edge prev_node r fd
       | Test (p,b)     -> tf_test var edge prev_node p b
-      | ASM (_, _, _)  -> tf_asm var edge prev_node (* TODO: use ASM fields for something? *)
+      | ASM (_, _, _,_)  -> tf_asm var edge prev_node (* TODO: use ASM fields for something? *)
       | Skip           -> tf_skip var edge prev_node
     end getl sidel getg sideg d
 
diff --git a/src/goblint.ml b/src/goblint.ml
index 4ea3a3d242..5b3e619434 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -59,7 +59,7 @@ let main () =
       (* This is run independant of the autotuner being enabled or not be sound for programs with longjmp *)
       AutoTune.activateLongjmpAnalysesWhenRequired ();
       if get_bool "ana.autotune.enabled" then AutoTune.chooseConfig file;
-      file |> do_analyze changeInfo;
+      file |> do_analyze changeInfo; 
       do_html_output ();
       do_gobview file;
       do_stats ();
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index d55eaf1c4f..b86cb807fe 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -399,8 +399,11 @@ let preprocess_files () =
 
   let preprocessed =
     List.concat_map preprocess_arg_file (List.map Fpath.v (get_string_list "files"))
+    (* todo: uncomment; for testing only *)
+    (*
     @
     List.concat_map (preprocess_arg_file ~preprocess:true) !extra_files
+    *)
   in
   if not (get_bool "pre.exist") then (
     let preprocess_tasks = List.filter_map snd preprocessed in
@@ -455,8 +458,6 @@ let parse_preprocessed preprocessed =
       Cilfacade.getAST preprocessed_file
     with
     | Frontc.ParseError s ->
-      if !E.hadErrors then
-        E.s (E.error "There were parsing errors in %s" fileName_str);
       raise (FrontendError (Format.sprintf "Frontc.ParseError: %s" s))
     | Errormsg.Error ->
       raise (FrontendError "Errormsg.Error")
@@ -556,7 +557,7 @@ let do_analyze change_info merged_AST =
         (* Cilfacade.current_file := ast'; *)
     in
 
-    Timing.wrap "analysis" (control_analyze merged_AST) funs
+    Timing.wrap "analysis" (control_analyze merged_AST) funs 
   )
 
 let do_html_output () =
diff --git a/src/transform/deadCode.ml b/src/transform/deadCode.ml
index 1b9db8d06a..35744ba27f 100644
--- a/src/transform/deadCode.ml
+++ b/src/transform/deadCode.ml
@@ -72,7 +72,7 @@ let filter_map_block ?(unchecked_condition = Fun.const (GoblintCil.integer 1)) f
         let keep_block = impl_block b in
         if keep_stmt || keep_block then Some skind else None
 
-      | Instr _ | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ as skind ->
+      | Instr _ | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ | Asm _ as skind ->
         (* no further statements are contained recursively here, so nothing left to do *)
         if keep_stmt then Some skind else None
 
@@ -91,7 +91,7 @@ let filter_map_block ?(unchecked_condition = Fun.const (GoblintCil.integer 1)) f
 (** Is it possible for this statement to begin executing normally, but not finish? *)
 let may_stop_execution stmt =
   match stmt.skind with
-  | Instr is -> List.exists (function Call _ | Asm _ -> true | _ -> false) is
+  | Instr is -> List.exists (function Call _ -> true | _ -> false) is
   | _ -> false
 
 (** Perform a depth first search over the CFG. Record the IDs of live statements;

From 43e50df234b7048a66c145a379c5b70678df31c4 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Sat, 25 Nov 2023 14:35:17 +0100
Subject: [PATCH 04/62] only added event type

---
 src/domains/events.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/domains/events.ml b/src/domains/events.ml
index 06561bddbe..375eb63236 100644
--- a/src/domains/events.ml
+++ b/src/domains/events.ml
@@ -16,6 +16,7 @@ type t =
   | Assert of exp
   | Unassume of {exp: CilType.Exp.t; uuids: string list}
   | Longjmped of {lval: CilType.Lval.t option}
+  | Invalidate of {lvals: CilType.Lval.t list}
 
 (** Should event be emitted after transfer function raises [Deadcode]? *)
 let emit_on_deadcode = function
@@ -31,7 +32,8 @@ let emit_on_deadcode = function
   | UpdateExpSplit _ (* Pointless to split on dead. *)
   | Unassume _ (* Avoid spurious writes. *)
   | Assert _ (* Pointless to refine dead. *)
-  | Longjmped _ ->
+  | Longjmped _
+  | Invalidate _ ->
     false
 
 let pretty () = function
@@ -47,3 +49,4 @@ let pretty () = function
   | Assert exp -> dprintf "Assert %a" d_exp exp
   | Unassume {exp; uuids} -> dprintf "Unassume {exp=%a; uuids=%a}" d_exp exp (docList Pretty.text) uuids
   | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval
+  | Invalidate {lvals} -> dprintf "Invalidate {vars=%a}" (docList (d_lval ())) lvals

From 5b09bbe4df65a48068401eba078a5d3a6692ffc2 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Sat, 25 Nov 2023 18:09:09 +0100
Subject: [PATCH 05/62] access analysis now emits invalidates

---
 src/analyses/accessAnalysis.ml | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index e99aefa0e5..53033640cc 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -25,9 +25,11 @@ struct
 
   let collect_local = ref false
   let emit_single_threaded = ref false
+  let ignore_asm = ref true
 
   let init _ =
     collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed";
+    ignore_asm := get_bool "asm_is_nop";
     let activated = get_string_list "ana.activated" in
     emit_single_threaded := List.mem (ModifiedSinceLongjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
 
@@ -73,6 +75,27 @@ struct
       ctx.local
     end
 
+  let asm (ctx: (D.t, G.t, C.t, V.t) ctx) : D.t =
+    if not !ignore_asm then
+      let asm_out, asm_in = 
+        match ctx.edge with
+        | ASM (_, asm_out, asm_in, _) ->
+          let third (_, _, x) = x in
+          List.map third asm_out,
+          List.map third asm_in
+        | _ -> failwith "transfer function asm called on non-asm edge"
+      in
+      let handle_in exp = 
+        match exp with
+        | Cil.Lval lval ->
+          if not (List.mem lval asm_out) then
+            access_one_top ~deref:true ctx Read false (AddrOf lval)
+          else ()
+        | _ -> access_one_top ctx Read false exp
+      in
+      List.iter handle_in asm_in;
+      ctx.emit (Events.Invalidate {lvals=asm_out})
+
   let branch ctx exp tv : D.t =
     access_one_top ctx Read false exp;
     ctx.local

From 343f51607a162bd72c39f07508fa04b935604302 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Wed, 29 Nov 2023 16:36:22 +0100
Subject: [PATCH 06/62] varEq analysis; invalidation tested

---
 src/analyses/varEq.ml               | 4 ++++
 src/common/util/options.schema.json | 6 ++++++
 2 files changed, 10 insertions(+)

diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index dcd49c9f02..2d9e884fd4 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -589,6 +589,10 @@ struct
           remove ask (Cil.var v) st
         in
         List.fold_left remove_var ctx.local (EscapeDomain.EscapedVars.elements vars)
+    | Invalidate {lvals} ->
+      let ask = Analyses.ask_of_ctx ctx in
+      let remove_lval ctx lval = remove ask lval ctx in
+      List.fold_left remove_lval ctx.local lvals
     | _ ->
       ctx.local
 end
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index 400dde06dc..23db580589 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/util/options.schema.json
@@ -17,6 +17,12 @@
       "type": "string",
       "default": ""
     },
+    "asm_is_nop": {
+      "title": "asm_is_nop",
+      "description": "treat asm statements as nop",
+      "type": "boolean",
+      "default": true
+    },
     "justcil": {
       "title": "justcil",
       "description": "Just parse and output the CIL.",

From e797b870d238a4faad7bdc999c74ae25277cadc4 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 30 Nov 2023 17:22:59 +0100
Subject: [PATCH 07/62] deadlock done; indentation complaints even after I ran
 ocp-indent???

---
 src/analyses/locksetAnalysis.ml | 32 ++++++++++++++++++++++++++++++++
 src/analyses/varEq.ml           |  2 +-
 src/framework/cfgTools.ml       | 12 ++++++++----
 3 files changed, 41 insertions(+), 5 deletions(-)

diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 2e9e08f03d..9ec12388c5 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -1,6 +1,7 @@
 (** Basic lockset analyses. *)
 
 open Analyses
+open GoblintCil
 
 
 module type DS =
@@ -33,6 +34,21 @@ sig
   val remove: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> D.t
 end
 
+let lock_of_lval (lhost, offset) =
+  match lhost with
+  | Var varinfo ->
+    let lock = ValueDomain.Addr.of_var varinfo in
+    let offset = Offset.Exp.of_cil offset in
+    let offset = ValueDomain.Offs.of_exp offset in
+    let lock = ValueDomain.Addr.add_offset lock offset in
+    Some lock
+  | Mem exp ->
+    match exp with
+    | Const (CInt (_, _, Some (str))) ->
+      let lock = ValueDomain.Addr.of_string str in
+      Some lock
+    | _ -> None
+
 module MakeMay (Arg: MayArg) =
 struct
   include Make (Arg.D)
@@ -51,6 +67,14 @@ struct
       ctx.local (* don't remove non-unique lock *)
     | Events.Unlock l ->
       Arg.remove ctx l (* remove definite lock or none in parallel if ambiguous *)
+    | Events.Invalidate {lvals} ->
+      let handle_lval ctx lval = 
+        match lock_of_lval lval with
+        | Some lock -> {ctx with local = Arg.remove ctx lock}
+        | None -> ctx
+      in
+      let ctx = List.fold_left handle_lval ctx lvals in
+      ctx.local
     | _ ->
       ctx.local
 end
@@ -82,6 +106,14 @@ struct
       Arg.remove_all ctx (* remove all locks *)
     | Events.Unlock l ->
       Arg.remove ctx l (* remove definite lock or all in parallel if ambiguous (blob lock is never added) *)
+    | Events.Invalidate {lvals} ->
+      let handle_lval ctx lval = 
+        match lock_of_lval lval with
+        | Some lock -> {ctx with local = Arg.remove ctx lock}
+        | None -> ctx
+      in
+      let ctx = List.fold_left handle_lval ctx lvals in
+      ctx.local
     | _ ->
       ctx.local
 end
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 2d9e884fd4..b93b1d3b03 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -589,7 +589,7 @@ struct
           remove ask (Cil.var v) st
         in
         List.fold_left remove_var ctx.local (EscapeDomain.EscapedVars.elements vars)
-    | Invalidate {lvals} ->
+    | Events.Invalidate {lvals} ->
       let ask = Analyses.ask_of_ctx ctx in
       let remove_lval ctx lval = remove ask lval ctx in
       List.fold_left remove_lval ctx.local lvals
diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
index 62b63570d3..e32a05dacb 100644
--- a/src/framework/cfgTools.ml
+++ b/src/framework/cfgTools.ml
@@ -145,6 +145,8 @@ 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
@@ -383,10 +385,12 @@ let createCFG (file: file) =
             | [] -> failwith "MyCFG.createCFG: 0 Asm succ"
             | [succ, skippedStatements] -> begin
                 addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, false)) (Statement succ);
-                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
+                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 ()
               end
             | _ -> failwith "MyCFG.createCFG: >1 Asm succ"
             end

From 834b50f4f88f3cf03debb95c8a829513473fe5b4 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Wed, 6 Dec 2023 14:28:14 +0100
Subject: [PATCH 08/62] mutexAnalysis done; fileUse buggy but commiting to try
 earlier commit

---
 src/analyses/deadlock.ml        |  2 ++
 src/analyses/fileUse.ml         | 18 +++++++++++++++++-
 src/analyses/locksetAnalysis.ml |  5 +++++
 src/analyses/mayLocks.ml        |  2 ++
 src/analyses/mutexAnalysis.ml   |  4 +++-
 5 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index c23d6f4294..d73600cefd 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -37,6 +37,8 @@ struct
         ) ctx.local;
       D.add after ctx.local
 
+    let warn_remove_unknown = ref true
+
     let remove ctx l =
       let inLockAddrs (e, _, _) = Lock.equal l e in
       D.filter (neg inLockAddrs) ctx.local
diff --git a/src/analyses/fileUse.ml b/src/analyses/fileUse.ml
index a9088a4bb2..03260ce01f 100644
--- a/src/analyses/fileUse.ml
+++ b/src/analyses/fileUse.ml
@@ -43,7 +43,6 @@ struct
     | [addr] -> Queries.AD.Addr.to_var_may addr
     | _ -> None
 
-
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
     let m = ctx.local in
@@ -286,6 +285,23 @@ struct
 
     | _ -> m
 
+
+  let event ctx e octx =
+    match e with
+    | Events.Invalidate {lvals} ->
+      let handle_lval dom lval =
+        let key = D.key_from_lval lval in
+        let keys = 
+          match D.get_alias key dom with
+          | Some k -> k::(D.get_aliased k dom)
+          | None -> []
+        in
+        let remove dom key = D.remove key dom in
+        List.fold remove dom keys
+      in
+      List.fold handle_lval ctx.local lvals
+    | _ -> ctx.local
+
   let startstate v = D.bot ()
   let threadenter ctx lval f args = [D.bot ()]
   let threadspawn ctx lval f args fctx = ctx.local
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 9ec12388c5..57384c6cdc 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -32,6 +32,7 @@ sig
 
   val add: (D.t, G.t, D.t, V.t) ctx -> LockDomain.Lockset.Lock.t -> D.t
   val remove: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> D.t
+  val warn_remove_unknown: bool ref
 end
 
 let lock_of_lval (lhost, offset) =
@@ -68,12 +69,14 @@ struct
     | Events.Unlock l ->
       Arg.remove ctx l (* remove definite lock or none in parallel if ambiguous *)
     | Events.Invalidate {lvals} ->
+      Arg.warn_remove_unknown := false;
       let handle_lval ctx lval = 
         match lock_of_lval lval with
         | Some lock -> {ctx with local = Arg.remove ctx lock}
         | None -> ctx
       in
       let ctx = List.fold_left handle_lval ctx lvals in
+      Arg.warn_remove_unknown := true;
       ctx.local
     | _ ->
       ctx.local
@@ -107,12 +110,14 @@ struct
     | Events.Unlock l ->
       Arg.remove ctx l (* remove definite lock or all in parallel if ambiguous (blob lock is never added) *)
     | Events.Invalidate {lvals} ->
+      Arg.warn_remove_unknown := false;
       let handle_lval ctx lval = 
         match lock_of_lval lval with
         | Some lock -> {ctx with local = Arg.remove ctx lock}
         | None -> ctx
       in
       let ctx = List.fold_left handle_lval ctx lvals in
+      Arg.warn_remove_unknown := true;
       ctx.local
     | _ ->
       ctx.local
diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml
index 853005de87..92f3a8aa35 100644
--- a/src/analyses/mayLocks.ml
+++ b/src/analyses/mayLocks.ml
@@ -29,6 +29,8 @@ struct
     else
       D.add l ctx.local
 
+  let warn_remove_unknown = ref true
+
   let remove ctx l =
     if not (D.mem l ctx.local) then M.warn "Releasing a mutex that is definitely not held";
     match D.Addr.to_mval l with
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index ee050f55ca..99a8676a3f 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -154,10 +154,12 @@ struct
         (s', Multiplicity.increment (fst l) m)
       | _ -> (s', m)
 
+    let warn_remove_unknown = ref true
+
     let remove' ctx ~warn l =
       let s, m = ctx.local in
       let rm s = Lockset.remove (l, true) (Lockset.remove (l, false) s) in
-      if warn &&  (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex (%a) which may not be held" Addr.pretty l;
+      if warn && !warn_remove_unknown &&  (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex (%a) which may not be held" Addr.pretty l;
       match Addr.to_mval l with
       | Some mval when MutexTypeAnalysis.must_be_recursive ctx mval ->
         let m',rmed = Multiplicity.decrement l m in

From 0605f4c24de481074bcc0034b33e4d361d4c32ae Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Wed, 13 Dec 2023 16:37:28 +0100
Subject: [PATCH 09/62] use queries

---
 src/analyses/deadlock.ml        |  8 +++--
 src/analyses/locksetAnalysis.ml | 62 ++++++++++++++++-----------------
 src/analyses/mayLocks.ml        |  4 +--
 src/analyses/mutexAnalysis.ml   |  6 ++--
 src/framework/analyses.ml       |  6 ++--
 5 files changed, 46 insertions(+), 40 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index d73600cefd..0c677c4112 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -37,11 +37,15 @@ struct
         ) ctx.local;
       D.add after ctx.local
 
-    let warn_remove_unknown = ref true
-
     let remove ctx l =
       let inLockAddrs (e, _, _) = Lock.equal l e in
       D.filter (neg inLockAddrs) ctx.local
+
+    let is_held ctx l =
+      let inLockAddrs (e, _, _) = Lock.equal l e in
+      M.msg_group Error ~category:Deadlock "FUCK" [];
+      D.exists inLockAddrs ctx.local
+      
   end
 
   include LocksetAnalysis.MakeMay (Arg)
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 57384c6cdc..328f4a81b1 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -32,24 +32,28 @@ sig
 
   val add: (D.t, G.t, D.t, V.t) ctx -> LockDomain.Lockset.Lock.t -> D.t
   val remove: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> D.t
-  val warn_remove_unknown: bool ref
+  val is_held: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> bool
 end
 
-let lock_of_lval (lhost, offset) =
-  match lhost with
-  | Var varinfo ->
-    let lock = ValueDomain.Addr.of_var varinfo in
-    let offset = Offset.Exp.of_cil offset in
-    let offset = ValueDomain.Offs.of_exp offset in
-    let lock = ValueDomain.Addr.add_offset lock offset in
-    Some lock
-  | Mem exp ->
-    match exp with
-    | Const (CInt (_, _, Some (str))) ->
-      let lock = ValueDomain.Addr.of_string str in
-      Some lock
-    | _ -> None
-
+let print_addr_set addr_set = Pretty.fprint stdout ~width:39 (ValueDomain.AD.pretty () addr_set)
+
+let addr_set_of_lval (a: Queries.ask) lval =
+  let exp = AddrOf lval in
+  let addr_set = a.f (Queries.MayPointTo exp) in
+  (* this doesn't work as I am forced to use AddrOf, otherwise MayPointTo returns garbage *)
+  (* if Queries.VD.is_mutex_type (ValueDomain.AD.type_of addr_set) then None
+  else Some addr_set *)
+  addr_set
+
+let locks_of_lvals ctx lvals =
+  let ask = Analyses.ask_of_ctx ctx in
+  let collect_addr_sets locks lval = 
+    let addr_set = addr_set_of_lval ask lval in
+    ValueDomain.AD.union locks addr_set 
+  in
+  let addr_set = List.fold_left collect_addr_sets (ValueDomain.AD.empty ()) lvals in
+  ValueDomain.AD.elements addr_set
+  
 module MakeMay (Arg: MayArg) =
 struct
   include Make (Arg.D)
@@ -69,14 +73,11 @@ struct
     | Events.Unlock l ->
       Arg.remove ctx l (* remove definite lock or none in parallel if ambiguous *)
     | Events.Invalidate {lvals} ->
-      Arg.warn_remove_unknown := false;
-      let handle_lval ctx lval = 
-        match lock_of_lval lval with
-        | Some lock -> {ctx with local = Arg.remove ctx lock}
-        | None -> ctx
-      in
-      let ctx = List.fold_left handle_lval ctx lvals in
-      Arg.warn_remove_unknown := true;
+      let locks = locks_of_lvals ctx lvals in
+      let is_held lock = Arg.is_held ctx lock in
+      let locks = List.filter is_held locks in
+      let remove_lock ctx lock = {ctx with local = Arg.remove ctx lock} in
+      let ctx = List.fold_left remove_lock ctx locks in
       ctx.local
     | _ ->
       ctx.local
@@ -110,14 +111,11 @@ struct
     | Events.Unlock l ->
       Arg.remove ctx l (* remove definite lock or all in parallel if ambiguous (blob lock is never added) *)
     | Events.Invalidate {lvals} ->
-      Arg.warn_remove_unknown := false;
-      let handle_lval ctx lval = 
-        match lock_of_lval lval with
-        | Some lock -> {ctx with local = Arg.remove ctx lock}
-        | None -> ctx
-      in
-      let ctx = List.fold_left handle_lval ctx lvals in
-      Arg.warn_remove_unknown := true;
+      let locks = locks_of_lvals ctx lvals in
+      let is_held lock = Arg.is_held ctx lock in
+      let locks = List.filter is_held locks in
+      let remove_lock ctx lock = {ctx with local = Arg.remove ctx lock} in
+      let ctx = List.fold_left remove_lock ctx locks in
       ctx.local
     | _ ->
       ctx.local
diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml
index 92f3a8aa35..bd1240a8e7 100644
--- a/src/analyses/mayLocks.ml
+++ b/src/analyses/mayLocks.ml
@@ -29,8 +29,6 @@ struct
     else
       D.add l ctx.local
 
-  let warn_remove_unknown = ref true
-
   let remove ctx l =
     if not (D.mem l ctx.local) then M.warn "Releasing a mutex that is definitely not held";
     match D.Addr.to_mval l with
@@ -40,6 +38,8 @@ struct
        | `Lifted MutexAttrDomain.MutexKind.NonRec -> D.remove l ctx.local
        | _ -> ctx.local (* we cannot remove them here *))
     | None -> ctx.local (* we cannot remove them here *)
+
+  let is_held ctx l = D.mem l ctx.local
 end
 
 module Spec =
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 99a8676a3f..9790d4c65d 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -154,12 +154,14 @@ struct
         (s', Multiplicity.increment (fst l) m)
       | _ -> (s', m)
 
-    let warn_remove_unknown = ref true
+    let is_held ctx l =
+      let s, _ = ctx.local in
+      Lockset.mem (l, true) s || Lockset.mem(l, false) s
 
     let remove' ctx ~warn l =
       let s, m = ctx.local in
       let rm s = Lockset.remove (l, true) (Lockset.remove (l, false) s) in
-      if warn && !warn_remove_unknown &&  (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex (%a) which may not be held" Addr.pretty l;
+      if warn && (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex (%a) which may not be held" Addr.pretty l;
       match Addr.to_mval l with
       | Some mval when MutexTypeAnalysis.must_be_recursive ctx mval ->
         let m',rmed = Multiplicity.decrement l m in
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index bb2170509d..1970ec2a58 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -643,8 +643,10 @@ struct
   let vdecl ctx _ = ctx.local
 
   let asm x =
-    M.msg_final Info ~category:Unsound "ASM ignored";
-    M.info ~category:Unsound "ASM statement ignored.";
+    if get_bool "asm_is_nop" then begin
+      M.msg_final Info ~category:Unsound "ASM ignored";
+      M.info ~category:Unsound "ASM statement ignored.";
+    end else ();
     x.local (* Just ignore. *)
 
   let skip x = x.local (* Just ignore. *)

From ccb8b05558adf4665ce90fe9244b4dabe95c0a6d Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 14 Dec 2023 11:43:37 +0100
Subject: [PATCH 10/62] warnings + expsplit (todo: ask supervisor about
 maylocks)

---
 src/analyses/deadlock.ml            |  8 ++++++--
 src/analyses/expsplit.ml            | 11 +++++++++++
 src/analyses/locksetAnalysis.ml     |  8 +++-----
 src/analyses/mayLocks.ml            |  8 +++++++-
 src/analyses/mutexAnalysis.ml       |  7 ++++++-
 src/common/util/messageCategory.ml  | 13 +++++++++++++
 src/common/util/options.schema.json | 18 ++++++++++++++++++
 7 files changed, 64 insertions(+), 9 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 0c677c4112..4e9869a104 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -37,13 +37,17 @@ struct
         ) ctx.local;
       D.add after ctx.local
 
-    let remove ctx l =
+    let remove ?(warn_clobber=false) ctx l =
+      if warn_clobber then
+        Messages.warn
+          ~category:MessageCategory.Deadlock
+          "Can't make assumptions about %a due to clobber" Lock.pretty l
+      else ();
       let inLockAddrs (e, _, _) = Lock.equal l e in
       D.filter (neg inLockAddrs) ctx.local
 
     let is_held ctx l =
       let inLockAddrs (e, _, _) = Lock.equal l e in
-      M.msg_group Error ~category:Deadlock "FUCK" [];
       D.exists inLockAddrs ctx.local
       
   end
diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml
index f121d0380e..0037f75872 100644
--- a/src/analyses/expsplit.ml
+++ b/src/analyses/expsplit.ml
@@ -96,6 +96,17 @@ struct
       D.add exp value ctx.local
     | Longjmped _ ->
       emit_splits_ctx ctx
+    | Invalidate {lvals} ->
+      let handle_lval local lval =
+        let exp = Lval lval in
+        if D.mem exp local then begin
+          Messages.warn
+            ~category:MessageCategory.Expsplit
+            "Can't make assumptions about %a due to clobber" Cil.d_lval lval;
+          D.remove exp local
+        end else local
+      in
+      List.fold handle_lval ctx.local lvals
     | _ ->
       ctx.local
 end
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 328f4a81b1..c3ec1a4b78 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -31,12 +31,10 @@ sig
   module V: SpecSysVar
 
   val add: (D.t, G.t, D.t, V.t) ctx -> LockDomain.Lockset.Lock.t -> D.t
-  val remove: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> D.t
+  val remove: ?warn_clobber:bool -> (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> D.t
   val is_held: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> bool
 end
 
-let print_addr_set addr_set = Pretty.fprint stdout ~width:39 (ValueDomain.AD.pretty () addr_set)
-
 let addr_set_of_lval (a: Queries.ask) lval =
   let exp = AddrOf lval in
   let addr_set = a.f (Queries.MayPointTo exp) in
@@ -76,7 +74,7 @@ struct
       let locks = locks_of_lvals ctx lvals in
       let is_held lock = Arg.is_held ctx lock in
       let locks = List.filter is_held locks in
-      let remove_lock ctx lock = {ctx with local = Arg.remove ctx lock} in
+      let remove_lock ctx lock = {ctx with local = Arg.remove ~warn_clobber:true ctx lock} in
       let ctx = List.fold_left remove_lock ctx locks in
       ctx.local
     | _ ->
@@ -114,7 +112,7 @@ struct
       let locks = locks_of_lvals ctx lvals in
       let is_held lock = Arg.is_held ctx lock in
       let locks = List.filter is_held locks in
-      let remove_lock ctx lock = {ctx with local = Arg.remove ctx lock} in
+      let remove_lock ctx lock = {ctx with local = Arg.remove ~warn_clobber:true ctx lock} in
       let ctx = List.fold_left remove_lock ctx locks in
       ctx.local
     | _ ->
diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml
index bd1240a8e7..952829720f 100644
--- a/src/analyses/mayLocks.ml
+++ b/src/analyses/mayLocks.ml
@@ -29,13 +29,19 @@ struct
     else
       D.add l ctx.local
 
-  let remove ctx l =
+  let remove ?(warn_clobber=false) ctx l =
+    if warn_clobber then
+      M.warn
+        ~category:MessageCategory.Maylocks
+        "Can't make assumptions about %a due to clobber" D.Addr.pretty l
+    else ();
     if not (D.mem l ctx.local) then M.warn "Releasing a mutex that is definitely not held";
     match D.Addr.to_mval l with
     | Some (v,o) ->
       (let mtype = ctx.ask (Queries.MutexType (v, Offset.Unit.of_offs o)) in
        match mtype with
        | `Lifted MutexAttrDomain.MutexKind.NonRec -> D.remove l ctx.local
+       (* todo: it's not removed -> ask supervisor about that *)
        | _ -> ctx.local (* we cannot remove them here *))
     | None -> ctx.local (* we cannot remove them here *)
 
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 9790d4c65d..876415875d 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -158,7 +158,12 @@ struct
       let s, _ = ctx.local in
       Lockset.mem (l, true) s || Lockset.mem(l, false) s
 
-    let remove' ctx ~warn l =
+    let remove' ?(warn_clobber=false) ctx ~warn l =
+      if warn && warn_clobber then
+        M.warn
+          ~category:MessageCategory.Multiplicity
+          "Can't make assumptions about %a due to clobber" Addr.pretty l
+      else ();
       let s, m = ctx.local in
       let rm s = Lockset.remove (l, true) (Lockset.remove (l, false) s) in
       if warn && (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex (%a) which may not be held" Addr.pretty l;
diff --git a/src/common/util/messageCategory.ml b/src/common/util/messageCategory.ml
index c70b8faf5f..c21cff53dd 100644
--- a/src/common/util/messageCategory.ml
+++ b/src/common/util/messageCategory.ml
@@ -46,6 +46,9 @@ type category =
   | Imprecise
   | Witness
   | Program
+  | Expsplit
+  | Multiplicity
+  | Maylocks
 [@@deriving eq, ord, hash]
 
 type t = category [@@deriving eq, ord, hash]
@@ -204,6 +207,9 @@ let should_warn e =
     | Imprecise -> "imprecise"
     | Witness -> "witness"
     | Program -> "program"
+    | Expsplit -> "expsplit"
+    | Multiplicity -> "multiplicity"
+    | Maylocks -> "maylocks"
     (* Don't forget to add option to schema! *)
   in get_bool ("warn." ^ (to_string e))
 
@@ -224,6 +230,9 @@ let path_show e =
   | Imprecise -> ["Imprecise"]
   | Witness -> ["Witness"]
   | Program -> ["Program"]
+  | Expsplit -> ["Expsplit"]
+  | Multiplicity -> ["Multiplicity"]
+  | Maylocks -> ["Maylocks"]
 
 let show x = String.concat " > " (path_show x)
 
@@ -263,6 +272,9 @@ let categoryName = function
       | Overflow -> "Overflow";
       | DivByZero -> "DivByZero")
   | Float -> "Float"
+  | Expsplit -> "Expsplit"
+  | Multiplicity -> "Multiplicity"
+  | Maylocks -> "Maylocks"
 
 
 let from_string_list (s: string list) =
@@ -283,6 +295,7 @@ let from_string_list (s: string list) =
     | "imprecise" -> Imprecise
     | "witness" -> Witness
     | "program" -> Program
+    | "expsplit" -> Expsplit
     | _ -> Unknown
 
 let to_yojson x = `List (List.map (fun x -> `String x) (path_show x))
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index 23db580589..d3b3aede98 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/util/options.schema.json
@@ -2111,6 +2111,24 @@
           "type": "boolean",
           "default": true
         },
+        "expsplit": {
+          "title": "warn.expsplit",
+          "description": "Expsplit messages",
+          "type": "boolean",
+          "default": true
+        },
+        "multiplicity": {
+          "title": "warn.multiplicity",
+          "description": "Multiplicity messages",
+          "type": "boolean",
+          "default": true
+        },
+        "maylocks": {
+          "title": "warn.maylocks",
+          "description": "Maylocks messages",
+          "type": "boolean",
+          "default": true
+        },
         "unknown": {
           "title": "warn.unknown",
           "description": "Unknown (of string) warnings",

From 16ca052bcbe2e0e26b3a43b5876810e8cb607c79 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 14 Dec 2023 13:36:03 +0100
Subject: [PATCH 11/62] this is only there to revert in case the warnings are
 needed (likely not)

---
 src/analyses/deadlock.ml            |  7 +------
 src/analyses/locksetAnalysis.ml     |  2 +-
 src/analyses/mayLocks.ml            |  7 +------
 src/analyses/mutexAnalysis.ml       |  7 +------
 src/common/util/messageCategory.ml  | 13 -------------
 src/common/util/options.schema.json | 18 ------------------
 6 files changed, 4 insertions(+), 50 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 4e9869a104..57078158ab 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -37,12 +37,7 @@ struct
         ) ctx.local;
       D.add after ctx.local
 
-    let remove ?(warn_clobber=false) ctx l =
-      if warn_clobber then
-        Messages.warn
-          ~category:MessageCategory.Deadlock
-          "Can't make assumptions about %a due to clobber" Lock.pretty l
-      else ();
+    let remove ctx l =
       let inLockAddrs (e, _, _) = Lock.equal l e in
       D.filter (neg inLockAddrs) ctx.local
 
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index c3ec1a4b78..605a481a32 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -31,7 +31,7 @@ sig
   module V: SpecSysVar
 
   val add: (D.t, G.t, D.t, V.t) ctx -> LockDomain.Lockset.Lock.t -> D.t
-  val remove: ?warn_clobber:bool -> (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> D.t
+  val remove: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> D.t
   val is_held: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> bool
 end
 
diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml
index 952829720f..b9e6f5d4f2 100644
--- a/src/analyses/mayLocks.ml
+++ b/src/analyses/mayLocks.ml
@@ -29,12 +29,7 @@ struct
     else
       D.add l ctx.local
 
-  let remove ?(warn_clobber=false) ctx l =
-    if warn_clobber then
-      M.warn
-        ~category:MessageCategory.Maylocks
-        "Can't make assumptions about %a due to clobber" D.Addr.pretty l
-    else ();
+  let remove ctx l =
     if not (D.mem l ctx.local) then M.warn "Releasing a mutex that is definitely not held";
     match D.Addr.to_mval l with
     | Some (v,o) ->
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 876415875d..9790d4c65d 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -158,12 +158,7 @@ struct
       let s, _ = ctx.local in
       Lockset.mem (l, true) s || Lockset.mem(l, false) s
 
-    let remove' ?(warn_clobber=false) ctx ~warn l =
-      if warn && warn_clobber then
-        M.warn
-          ~category:MessageCategory.Multiplicity
-          "Can't make assumptions about %a due to clobber" Addr.pretty l
-      else ();
+    let remove' ctx ~warn l =
       let s, m = ctx.local in
       let rm s = Lockset.remove (l, true) (Lockset.remove (l, false) s) in
       if warn && (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex (%a) which may not be held" Addr.pretty l;
diff --git a/src/common/util/messageCategory.ml b/src/common/util/messageCategory.ml
index c21cff53dd..c70b8faf5f 100644
--- a/src/common/util/messageCategory.ml
+++ b/src/common/util/messageCategory.ml
@@ -46,9 +46,6 @@ type category =
   | Imprecise
   | Witness
   | Program
-  | Expsplit
-  | Multiplicity
-  | Maylocks
 [@@deriving eq, ord, hash]
 
 type t = category [@@deriving eq, ord, hash]
@@ -207,9 +204,6 @@ let should_warn e =
     | Imprecise -> "imprecise"
     | Witness -> "witness"
     | Program -> "program"
-    | Expsplit -> "expsplit"
-    | Multiplicity -> "multiplicity"
-    | Maylocks -> "maylocks"
     (* Don't forget to add option to schema! *)
   in get_bool ("warn." ^ (to_string e))
 
@@ -230,9 +224,6 @@ let path_show e =
   | Imprecise -> ["Imprecise"]
   | Witness -> ["Witness"]
   | Program -> ["Program"]
-  | Expsplit -> ["Expsplit"]
-  | Multiplicity -> ["Multiplicity"]
-  | Maylocks -> ["Maylocks"]
 
 let show x = String.concat " > " (path_show x)
 
@@ -272,9 +263,6 @@ let categoryName = function
       | Overflow -> "Overflow";
       | DivByZero -> "DivByZero")
   | Float -> "Float"
-  | Expsplit -> "Expsplit"
-  | Multiplicity -> "Multiplicity"
-  | Maylocks -> "Maylocks"
 
 
 let from_string_list (s: string list) =
@@ -295,7 +283,6 @@ let from_string_list (s: string list) =
     | "imprecise" -> Imprecise
     | "witness" -> Witness
     | "program" -> Program
-    | "expsplit" -> Expsplit
     | _ -> Unknown
 
 let to_yojson x = `List (List.map (fun x -> `String x) (path_show x))
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index d3b3aede98..23db580589 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/util/options.schema.json
@@ -2111,24 +2111,6 @@
           "type": "boolean",
           "default": true
         },
-        "expsplit": {
-          "title": "warn.expsplit",
-          "description": "Expsplit messages",
-          "type": "boolean",
-          "default": true
-        },
-        "multiplicity": {
-          "title": "warn.multiplicity",
-          "description": "Multiplicity messages",
-          "type": "boolean",
-          "default": true
-        },
-        "maylocks": {
-          "title": "warn.maylocks",
-          "description": "Maylocks messages",
-          "type": "boolean",
-          "default": true
-        },
         "unknown": {
           "title": "warn.unknown",
           "description": "Unknown (of string) warnings",

From 26c3dc636138680785ba72df5c21c61845ad52e5 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 14 Dec 2023 13:38:46 +0100
Subject: [PATCH 12/62] ups

---
 src/analyses/expsplit.ml        | 3 ---
 src/analyses/locksetAnalysis.ml | 4 ++--
 2 files changed, 2 insertions(+), 5 deletions(-)

diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml
index 0037f75872..efcaf9d319 100644
--- a/src/analyses/expsplit.ml
+++ b/src/analyses/expsplit.ml
@@ -100,9 +100,6 @@ struct
       let handle_lval local lval =
         let exp = Lval lval in
         if D.mem exp local then begin
-          Messages.warn
-            ~category:MessageCategory.Expsplit
-            "Can't make assumptions about %a due to clobber" Cil.d_lval lval;
           D.remove exp local
         end else local
       in
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 605a481a32..5630b92450 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -74,7 +74,7 @@ struct
       let locks = locks_of_lvals ctx lvals in
       let is_held lock = Arg.is_held ctx lock in
       let locks = List.filter is_held locks in
-      let remove_lock ctx lock = {ctx with local = Arg.remove ~warn_clobber:true ctx lock} in
+      let remove_lock ctx lock = {ctx with local = Arg.remove ctx lock} in
       let ctx = List.fold_left remove_lock ctx locks in
       ctx.local
     | _ ->
@@ -112,7 +112,7 @@ struct
       let locks = locks_of_lvals ctx lvals in
       let is_held lock = Arg.is_held ctx lock in
       let locks = List.filter is_held locks in
-      let remove_lock ctx lock = {ctx with local = Arg.remove ~warn_clobber:true ctx lock} in
+      let remove_lock ctx lock = {ctx with local = Arg.remove ctx lock} in
       let ctx = List.fold_left remove_lock ctx locks in
       ctx.local
     | _ ->

From 22276ada4056eaf4c97400ad3602d99a53e8a994 Mon Sep 17 00:00:00 2001
From: ge46lup <ge46lup@tum.de>
Date: Thu, 14 Dec 2023 13:51:41 +0100
Subject: [PATCH 13/62] mallocFresh

---
 src/analyses/mallocFresh.ml   | 14 ++++++++++++--
 src/common/util/cilfacade0.ml |  1 +
 tests/practical/test_file     | 26 ++++++++++++++++++++++++++
 3 files changed, 39 insertions(+), 2 deletions(-)
 create mode 100755 tests/practical/test_file

diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index 3a501fc72f..a61da9e465 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -9,7 +9,12 @@ struct
   include Analyses.IdentitySpec
 
   (* must fresh variables *)
-  module D = SetDomain.Reverse (SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All variables" end)) (* need bot (top) for hoare widen *)
+  (*module D = SetDomain.Reverse (SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All variables" end)) (* need bot (top) for hoare widen *)
+  *)
+  module D = SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All variables" end)
+
+  
+  
   module C = D
 
   let name () = "mallocFresh"
@@ -21,7 +26,12 @@ struct
     match ask.f (MayPointTo (AddrOf lval)) with
     | ad when Queries.AD.is_top ad -> D.empty ()
     | ad when Queries.AD.exists (function
-        | Queries.AD.Addr.Addr (v,_) -> not (D.mem v local) && (v.vglob || ThreadEscape.has_escaped ask v)
+        (*| Queries.AD.Addr.Addr (v,_) -> not (D.mem v local) && (v.vglob || ThreadEscape.has_escaped ask v)*)
+        | Queries.AD.Addr.Addr (v,_) ->
+          if D.mem (v, false) local then
+            D.add (v, true) local  (* Invalidate the variable *)
+          else
+            local
         | _ -> false
       ) ad -> D.empty ()
     | _ -> local
diff --git a/src/common/util/cilfacade0.ml b/src/common/util/cilfacade0.ml
index 989d0bd316..a153dab3ab 100644
--- a/src/common/util/cilfacade0.ml
+++ b/src/common/util/cilfacade0.ml
@@ -30,6 +30,7 @@ let get_instrLoc = function
   | Set (_, _, loc, eloc) -> eloc_fallback ~eloc ~loc
   | Call (_, _, _, loc, eloc) -> eloc_fallback ~eloc ~loc
   | VarDecl (_, loc) -> loc
+  
 
 (** Get expression location for [Cil.stmt]. *)
 (* confusingly CIL.get_stmtLoc works on stmtkind instead *)
diff --git a/tests/practical/test_file b/tests/practical/test_file
new file mode 100755
index 0000000000..107600c3dd
--- /dev/null
+++ b/tests/practical/test_file
@@ -0,0 +1,26 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+void allocateMemory() {
+    int *ptr = malloc(sizeof(int));
+    
+    if (ptr != NULL) {
+        *ptr = 42;
+
+        // Your code that uses 'ptr'
+
+        printf("Value: %d\n", *ptr);
+
+        free(ptr);
+    } else {
+        fprintf(stderr, "Memory allocation failed.\n");
+    }
+}
+
+int main() {
+    allocateMemory();
+
+    // Additional code if needed
+
+    return 0;
+}

From 6925cbc0c7e7455e5f201f365c80bfadb54b13af Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Wed, 20 Dec 2023 16:50:25 +0100
Subject: [PATCH 14/62] memLeak; ask supervisor about Multiple query

---
 src/analyses/mayLocks.ml |  3 ++-
 src/analyses/memLeak.ml  | 40 +++++++++++++++++++++++++++++++---------
 2 files changed, 33 insertions(+), 10 deletions(-)

diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml
index b9e6f5d4f2..8485243173 100644
--- a/src/analyses/mayLocks.ml
+++ b/src/analyses/mayLocks.ml
@@ -30,13 +30,14 @@ struct
       D.add l ctx.local
 
   let remove ctx l =
+    Pretty.fprint stdout ~width:69 (D.Addr.pretty () l);
     if not (D.mem l ctx.local) then M.warn "Releasing a mutex that is definitely not held";
     match D.Addr.to_mval l with
     | Some (v,o) ->
       (let mtype = ctx.ask (Queries.MutexType (v, Offset.Unit.of_offs o)) in
        match mtype with
        | `Lifted MutexAttrDomain.MutexKind.NonRec -> D.remove l ctx.local
-       (* todo: it's not removed -> ask supervisor about that *)
+       (* todo [IMPORTANT]: find out why the else branch is always taken at invalidate *)
        | _ -> ctx.local (* we cannot remove them here *))
     | None -> ctx.local (* we cannot remove them here *)
 
diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index dbaa2d69fc..6599365ac3 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -45,6 +45,17 @@ struct
     if f.svar.vname = "main" then check_for_mem_leak ctx;
     ctx.local
 
+  let heapvar_from_ptr_opt ctx ptr = 
+    begin match ctx.ask (Queries.MayPointTo ptr) with
+      | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad = 1 ->
+        (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *)
+        begin match Queries.AD.choose ad with
+          | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) (* todo: ask supervisor && not @@ ctx.ask (Queries.IsMultiple v) *) -> Some v
+          | _ -> None
+        end
+      | _ -> None
+    end
+
   let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t =
     let state = ctx.local in
     let desc = LibraryFunctions.find f in
@@ -59,14 +70,9 @@ struct
         | _ -> state
       end
     | Free ptr ->
-      begin match ctx.ask (Queries.MayPointTo ptr) with
-        | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad = 1 ->
-          (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *)
-          begin match Queries.AD.choose ad with
-            | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> D.remove v state (* Unique pointed to heap vars *)
-            | _ -> state
-          end
-        | _ -> state
+      begin match heapvar_from_ptr_opt ctx ptr with
+        | Some v -> D.remove v state
+        | None -> state
       end
     | Abort ->
       (* An "Abort" special function indicates program exit => need to check for memory leaks *)
@@ -90,9 +96,25 @@ struct
       state
     | _ -> state
 
+  let event ctx e octx =
+    match e with
+    | Events.Invalidate {lvals} ->
+      let old_state = ctx.local in
+      let handle_lval ctx lval =
+        let state = ctx.local in
+        match heapvar_from_ptr_opt ctx (Lval lval) with
+        | Some v -> {ctx with local = D.remove v state}
+        | None -> ctx
+      in
+      let ctx = List.fold_left handle_lval ctx lvals in
+      let ctx' = {ctx with local = D.diff old_state ctx.local} in
+      check_for_mem_leak ctx';
+      ctx.local
+    | _ -> ctx.local
+
   let startstate v = D.bot ()
   let exitstate v = D.top ()
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
\ No newline at end of file
+  MCP.register_analysis (module Spec : MCPSpec)

From 7f63076a1a60a3efe6ca82a2782f0f013052756c Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Wed, 20 Dec 2023 16:51:57 +0100
Subject: [PATCH 15/62] Revert "mallocFresh" => revert the revert when it
 compiles pls

This reverts commit 22276ada4056eaf4c97400ad3602d99a53e8a994.
---
 src/analyses/mallocFresh.ml   | 14 ++------------
 src/common/util/cilfacade0.ml |  1 -
 tests/practical/test_file     | 26 --------------------------
 3 files changed, 2 insertions(+), 39 deletions(-)
 delete mode 100755 tests/practical/test_file

diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index a61da9e465..3a501fc72f 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -9,12 +9,7 @@ struct
   include Analyses.IdentitySpec
 
   (* must fresh variables *)
-  (*module D = SetDomain.Reverse (SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All variables" end)) (* need bot (top) for hoare widen *)
-  *)
-  module D = SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All variables" end)
-
-  
-  
+  module D = SetDomain.Reverse (SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All variables" end)) (* need bot (top) for hoare widen *)
   module C = D
 
   let name () = "mallocFresh"
@@ -26,12 +21,7 @@ struct
     match ask.f (MayPointTo (AddrOf lval)) with
     | ad when Queries.AD.is_top ad -> D.empty ()
     | ad when Queries.AD.exists (function
-        (*| Queries.AD.Addr.Addr (v,_) -> not (D.mem v local) && (v.vglob || ThreadEscape.has_escaped ask v)*)
-        | Queries.AD.Addr.Addr (v,_) ->
-          if D.mem (v, false) local then
-            D.add (v, true) local  (* Invalidate the variable *)
-          else
-            local
+        | Queries.AD.Addr.Addr (v,_) -> not (D.mem v local) && (v.vglob || ThreadEscape.has_escaped ask v)
         | _ -> false
       ) ad -> D.empty ()
     | _ -> local
diff --git a/src/common/util/cilfacade0.ml b/src/common/util/cilfacade0.ml
index a153dab3ab..989d0bd316 100644
--- a/src/common/util/cilfacade0.ml
+++ b/src/common/util/cilfacade0.ml
@@ -30,7 +30,6 @@ let get_instrLoc = function
   | Set (_, _, loc, eloc) -> eloc_fallback ~eloc ~loc
   | Call (_, _, _, loc, eloc) -> eloc_fallback ~eloc ~loc
   | VarDecl (_, loc) -> loc
-  
 
 (** Get expression location for [Cil.stmt]. *)
 (* confusingly CIL.get_stmtLoc works on stmtkind instead *)
diff --git a/tests/practical/test_file b/tests/practical/test_file
deleted file mode 100755
index 107600c3dd..0000000000
--- a/tests/practical/test_file
+++ /dev/null
@@ -1,26 +0,0 @@
-#include <stdio.h>
-#include <stdlib.h>
-
-void allocateMemory() {
-    int *ptr = malloc(sizeof(int));
-    
-    if (ptr != NULL) {
-        *ptr = 42;
-
-        // Your code that uses 'ptr'
-
-        printf("Value: %d\n", *ptr);
-
-        free(ptr);
-    } else {
-        fprintf(stderr, "Memory allocation failed.\n");
-    }
-}
-
-int main() {
-    allocateMemory();
-
-    // Additional code if needed
-
-    return 0;
-}

From d45791be46ef6140d16ae7ed9fd744aaf0430893 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 21 Dec 2023 10:36:16 +0100
Subject: [PATCH 16/62] should have done base earlier; lots of analyses solve
 themselves

---
 src/analyses/base.ml            |  3 +++
 src/analyses/locksetAnalysis.ml |  5 +----
 src/analyses/mayLocks.ml        |  1 -
 src/analyses/memLeak.ml         | 18 +-----------------
 4 files changed, 5 insertions(+), 22 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 6536a9c496..4745212446 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2828,6 +2828,9 @@ struct
           {st' with cpa = CPA.remove !longjmp_return st'.cpa}
         | None -> ctx.local
       end
+    | Events.Invalidate {lvals} ->
+      let exps = List.map Cil.mkAddrOrStartOf lvals in
+      invalidate ~ctx (Analyses.ask_of_ctx ctx) ctx.global st exps
     | _ ->
       ctx.local
 end
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 5630b92450..27b93a8fc3 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -36,11 +36,8 @@ sig
 end
 
 let addr_set_of_lval (a: Queries.ask) lval =
-  let exp = AddrOf lval in
+  let exp = Cil.mkAddrOrStartOf lval in
   let addr_set = a.f (Queries.MayPointTo exp) in
-  (* this doesn't work as I am forced to use AddrOf, otherwise MayPointTo returns garbage *)
-  (* if Queries.VD.is_mutex_type (ValueDomain.AD.type_of addr_set) then None
-  else Some addr_set *)
   addr_set
 
 let locks_of_lvals ctx lvals =
diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml
index 8485243173..0a0e39e898 100644
--- a/src/analyses/mayLocks.ml
+++ b/src/analyses/mayLocks.ml
@@ -30,7 +30,6 @@ struct
       D.add l ctx.local
 
   let remove ctx l =
-    Pretty.fprint stdout ~width:69 (D.Addr.pretty () l);
     if not (D.mem l ctx.local) then M.warn "Releasing a mutex that is definitely not held";
     match D.Addr.to_mval l with
     | Some (v,o) ->
diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index 6599365ac3..fa66f2e9cf 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -50,7 +50,7 @@ struct
       | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad = 1 ->
         (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *)
         begin match Queries.AD.choose ad with
-          | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) (* todo: ask supervisor && not @@ ctx.ask (Queries.IsMultiple v) *) -> Some v
+          | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> Some v
           | _ -> None
         end
       | _ -> None
@@ -96,22 +96,6 @@ struct
       state
     | _ -> state
 
-  let event ctx e octx =
-    match e with
-    | Events.Invalidate {lvals} ->
-      let old_state = ctx.local in
-      let handle_lval ctx lval =
-        let state = ctx.local in
-        match heapvar_from_ptr_opt ctx (Lval lval) with
-        | Some v -> {ctx with local = D.remove v state}
-        | None -> ctx
-      in
-      let ctx = List.fold_left handle_lval ctx lvals in
-      let ctx' = {ctx with local = D.diff old_state ctx.local} in
-      check_for_mem_leak ctx';
-      ctx.local
-    | _ -> ctx.local
-
   let startstate v = D.bot ()
   let exitstate v = D.top ()
 end

From 08a7156171a2f9ab92385ed5392e9dd05c9b1409 Mon Sep 17 00:00:00 2001
From: ge46lup <ge46lup@tum.de>
Date: Thu, 21 Dec 2023 12:02:24 +0100
Subject: [PATCH 17/62] malloc Fresh

---
 src/analyses/mallocFresh.ml | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index 3a501fc72f..31e91e5bb0 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -29,6 +29,23 @@ struct
   let assign ctx lval rval =
     assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
+    let is_relevant_variable v =
+      (* Check if the variable is a global variable *)
+      v.vglob
+    
+    let event ctx e octx =
+        match e with
+        | Events.Invalidate {lvals} ->
+          (* Perform invalidation for mallocFresh analysis *)
+          let updated_locals = List.fold_left (fun acc lval ->
+            (* Check if lval is relevant to mallocFresh analysis and update the domain accordingly *)
+            match lval with
+            | (Var v, _) when is_relevant_variable v -> D.remove v acc
+            | _ -> acc
+          ) ctx.local lvals in
+          updated_locals
+        | _ -> ctx.local  
+
   let combine_env ctx lval fexp f args fc au f_ask =
     ctx.local (* keep local as opposed to IdentitySpec *)
 

From 4bc2e6724ffccdc0c3a27a3f0cde7075a364cb87 Mon Sep 17 00:00:00 2001
From: ge46lup <ge46lup@tum.de>
Date: Mon, 8 Jan 2024 09:18:06 +0100
Subject: [PATCH 18/62] region-analysis

---
 src/analyses/region.ml | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 6d2ae246c3..916a08e4a4 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -58,6 +58,21 @@ struct
         ls
     | _ -> Queries.Result.top q
 
+    let event ctx e octx =
+      match e with
+      | Events.Invalidate {lvals} ->
+        begin
+          match ctx.local with
+          | `Lifted reg ->
+            let invalidation_set = Lvals.of_list lvals in
+            let updated_reg = RegMap.mapi (fun v r ->
+              if Lvals.mem v invalidation_set then RegPart.top () else r
+            ) reg in
+            `Lifted updated_reg
+          | _ -> ctx.local
+        end
+      | _ -> ctx.local  
+
   module Lvals = SetDomain.Make (Mval.Exp)
   module A =
   struct
@@ -185,4 +200,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCP.register_analysis ~events:[Spec.event] (module Spec : MCPSpec)

From eb1650b16d871a94905c737ed85b69c2442befb6 Mon Sep 17 00:00:00 2001
From: ge46lup <ge46lup@tum.de>
Date: Tue, 9 Jan 2024 16:11:17 +0100
Subject: [PATCH 19/62] i add event function to region and useAfterfree
 analysis but it doesnt compile

---
 src/analyses/region.ml       | 32 ++++++++++++++++++--------------
 src/analyses/useAfterFree.ml | 17 ++++++++++++++---
 tests/practical/test_file    | 16 ++++++++++++++++
 3 files changed, 48 insertions(+), 17 deletions(-)
 create mode 100644 tests/practical/test_file

diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 916a08e4a4..f789e422f2 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -58,20 +58,7 @@ struct
         ls
     | _ -> Queries.Result.top q
 
-    let event ctx e octx =
-      match e with
-      | Events.Invalidate {lvals} ->
-        begin
-          match ctx.local with
-          | `Lifted reg ->
-            let invalidation_set = Lvals.of_list lvals in
-            let updated_reg = RegMap.mapi (fun v r ->
-              if Lvals.mem v invalidation_set then RegPart.top () else r
-            ) reg in
-            `Lifted updated_reg
-          | _ -> ctx.local
-        end
-      | _ -> ctx.local  
+    
 
   module Lvals = SetDomain.Make (Mval.Exp)
   module A =
@@ -90,6 +77,23 @@ struct
       | Some r when Lvals.is_empty r -> false
       | _ -> true
   end
+
+
+  let event ctx e octx =
+    match e with
+    | Events.Invalidate {lvals} ->
+      begin
+        match ctx.local with
+        | `Lifted reg ->
+          let invalidation_set = Lvals.of_list lvals in
+          let updated_reg = RegMap.mapi (fun v r ->
+            if Lvals.mem v invalidation_set then RegPart.top () else r
+          ) reg in
+          `Lifted updated_reg
+        | _ -> ctx.local
+      end
+    | _ -> ctx.local  
+
   let access ctx (a: Queries.access) =
     match a with
     | Point ->
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index ef63ab3e91..325f1876ca 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -25,8 +25,18 @@ struct
   module V = VarinfoV
 
   let context _ _ = ()
-
-
+ 
+  
+  
+  let event_function (ctx: (D.t, G.t, C.t, V.t) ctx) (event: Events.t) : (D.t * D.t) =
+    match event with
+    | Events.Invalidate { lvals } ->
+      (* Remove invalidated or freed heap variables from the heSap state *)
+      let heap_state = snd ctx.local in
+      let updated_heap_state = List.fold_left (fun heap_state lval -> D.remove lval heap_state) heap_state lvals in
+      (fst ctx.local, updated_heap_state)
+    | _ -> ctx.local
+  
   (* HELPER FUNCTIONS *)
 
   let get_current_threadid ctx =
@@ -243,4 +253,5 @@ struct
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
\ No newline at end of file
+  
+  MCP.register_analysis ~events:[event_function] (module Spec : MCPSpec)
\ No newline at end of file
diff --git a/tests/practical/test_file b/tests/practical/test_file
new file mode 100644
index 0000000000..4eae6d8ae4
--- /dev/null
+++ b/tests/practical/test_file
@@ -0,0 +1,16 @@
+#include <stdlib.h>
+
+int main() {
+    int *ptr = (int *)malloc(sizeof(int));
+
+    // Access allocated memory
+    *ptr = 42;
+
+    // Free the allocated memory
+    free(ptr);
+
+    // Access the freed memory (use-after-free)
+    int value = *ptr;  // This should trigger a use-after-free warning
+
+    return 0;
+}

From 208417395e408fb467b990d54a3052c274792b72 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Konrad=20G=C3=B6=C3=9Fmann?= <konrad.goessmann@tum.de>
Date: Thu, 11 Jan 2024 11:58:08 +0100
Subject: [PATCH 20/62] Modifes Taint jmpbufs to store if potentially invalid.
 Warns upon longjump to invalid Jumpbuf

---
 src/analyses/base.ml         |  7 +++++--
 src/cdomains/jmpBufDomain.ml | 11 ++++++-----
 src/cdomains/valueDomain.ml  | 10 +++++-----
 3 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 4745212446..7118b6a2b7 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1229,9 +1229,12 @@ struct
           if AD.mem Addr.UnknownPtr jmp_buf then
             M.warn ~category:Imprecise "Jump buffer %a may contain unknown pointers." d_exp e;
           begin match get ~top:(VD.bot ()) (Analyses.ask_of_ctx ctx) ctx.global ctx.local jmp_buf None with
-            | JmpBuf (x, copied) ->
+            | JmpBuf (x, copied, invalid) ->
               if copied then
                 M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e;
+              (* M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a was modified by inline assembly. This is may lead to Undefined Behavior." d_exp e; *)
+              if invalid then
+                M.warn ~category:(Behavior (Undefined Other)) "The jump target %a may have been altered in an inline assembly block." d_exp e;
               x
             | Top
             | Bot ->
@@ -2477,7 +2480,7 @@ struct
       let ask = Analyses.ask_of_ctx ctx in
       let st' = match eval_rv ask gs st env with
         | Address jmp_buf ->
-          let value = VD.JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, ctx.control_context ())), false) in
+          let value = VD.JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, ctx.control_context ())), false, false) in
           let r = set ~ctx ask gs st jmp_buf (Cilfacade.typeOf env) value in
           if M.tracing then M.tracel "setjmp" "setting setjmp %a on %a -> %a\n" d_exp env D.pretty st D.pretty r;
           r
diff --git a/src/cdomains/jmpBufDomain.ml b/src/cdomains/jmpBufDomain.ml
index 3c94fa8f47..f2ef201c34 100644
--- a/src/cdomains/jmpBufDomain.ml
+++ b/src/cdomains/jmpBufDomain.ml
@@ -37,13 +37,14 @@ struct
   let meet = inter
 end
 
-module JmpBufSetTaint =
+module JmpBufSetTaintInvalid =
 struct
   module Bufs = JmpBufSet
-  include Lattice.Prod(JmpBufSet)(BoolDomain.MayBool)
-  let buffers (a,_) = a
-  let copied (_,b) = b
-  let name () = "JumpbufferCopyTaint"
+  include Lattice.Prod3(JmpBufSet)(BoolDomain.MayBool)(BoolDomain.MayBool)
+  let buffers (buffer,_,_) = buffer
+  let copied (_,copied,_) = copied
+  let invalid (_,_,invalid) = invalid
+  let name () = "JumpbufferTaintOrInvalid"
 end
 
 
diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index cba4b04c18..114a51e88f 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -74,7 +74,7 @@ struct
 end
 
 module Threads = ConcDomain.ThreadSet
-module JmpBufs = JmpBufDomain.JmpBufSetTaint
+module JmpBufs = JmpBufDomain.JmpBufSetTaintInvalid
 
 module rec Compound: sig
   type t =
@@ -148,7 +148,7 @@ struct
       Array (CArrays.make ~varAttr ~typAttr len (bot_value ai))
     | t when is_thread_type t -> Thread (ConcDomain.ThreadSet.empty ())
     | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.bot ())
-    | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.Bufs.empty (), false)
+    | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.Bufs.empty (), false, false)
     | TNamed ({ttype=t; _}, _) -> bot_value ~varAttr (unrollType t)
     | _ -> Bot
 
@@ -709,7 +709,7 @@ struct
       Array (CArrays.set ask n (array_idx_top) v)
     |                 t , Blob n       -> Blob (Blobs.invalidate_value ask t n)
     |                 _ , Thread _     -> state (* TODO: no top thread ID set! *)
-    |                 _ , JmpBuf _     -> state (* TODO: no top jmpbuf *)
+    |                 _ , JmpBuf (b, c, _)     -> JmpBuf(b, c, true) (* TODO: no top jmpbuf *)
     | _, Bot -> Bot (* Leave uninitialized value (from malloc) alone in free to avoid trashing everything. TODO: sound? *)
     |                 t , _             -> top_value t
 
@@ -974,7 +974,7 @@ struct
             | Blob(Bot, _, _) -> Bot (* TODO: Stopgap for malloced jmp_bufs, there is something fundamentally flawed somewhere *)
             | _ ->
               if !AnalysisState.global_initialization then
-                JmpBuf (JmpBufs.Bufs.empty (), false) (* if assigning global init, use empty set instead *)
+                JmpBuf (JmpBufs.Bufs.empty (), false, false) (* if assigning global init, use empty set instead *)
               else
                 Top
           end
@@ -1139,7 +1139,7 @@ struct
 
   let rec mark_jmpbufs_as_copied (v:t):t =
     match v with
-    | JmpBuf (v,t) -> JmpBuf (v, true)
+    | JmpBuf (v,t,i) -> JmpBuf (v, true, i)
     | Array n -> Array (CArrays.map (fun (x: t) -> mark_jmpbufs_as_copied x) n)
     | Struct n -> Struct (Structs.map (fun (x: t) -> mark_jmpbufs_as_copied x) n)
     | Union (f, n) -> Union (f, mark_jmpbufs_as_copied n)

From e5cbbbc3f4d2661637ddae15b7703d2c8a854a85 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 11 Jan 2024 15:26:44 +0100
Subject: [PATCH 21/62] Revert commit that doesn't compile so that we can test

This reverts commit eb1650b16d871a94905c737ed85b69c2442befb6.
---
 src/analyses/region.ml       | 32 ++++++++++++++------------------
 src/analyses/useAfterFree.ml | 17 +++--------------
 tests/practical/test_file    | 16 ----------------
 3 files changed, 17 insertions(+), 48 deletions(-)
 delete mode 100644 tests/practical/test_file

diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index f789e422f2..916a08e4a4 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -58,7 +58,20 @@ struct
         ls
     | _ -> Queries.Result.top q
 
-    
+    let event ctx e octx =
+      match e with
+      | Events.Invalidate {lvals} ->
+        begin
+          match ctx.local with
+          | `Lifted reg ->
+            let invalidation_set = Lvals.of_list lvals in
+            let updated_reg = RegMap.mapi (fun v r ->
+              if Lvals.mem v invalidation_set then RegPart.top () else r
+            ) reg in
+            `Lifted updated_reg
+          | _ -> ctx.local
+        end
+      | _ -> ctx.local  
 
   module Lvals = SetDomain.Make (Mval.Exp)
   module A =
@@ -77,23 +90,6 @@ struct
       | Some r when Lvals.is_empty r -> false
       | _ -> true
   end
-
-
-  let event ctx e octx =
-    match e with
-    | Events.Invalidate {lvals} ->
-      begin
-        match ctx.local with
-        | `Lifted reg ->
-          let invalidation_set = Lvals.of_list lvals in
-          let updated_reg = RegMap.mapi (fun v r ->
-            if Lvals.mem v invalidation_set then RegPart.top () else r
-          ) reg in
-          `Lifted updated_reg
-        | _ -> ctx.local
-      end
-    | _ -> ctx.local  
-
   let access ctx (a: Queries.access) =
     match a with
     | Point ->
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 325f1876ca..ef63ab3e91 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -25,18 +25,8 @@ struct
   module V = VarinfoV
 
   let context _ _ = ()
- 
-  
-  
-  let event_function (ctx: (D.t, G.t, C.t, V.t) ctx) (event: Events.t) : (D.t * D.t) =
-    match event with
-    | Events.Invalidate { lvals } ->
-      (* Remove invalidated or freed heap variables from the heSap state *)
-      let heap_state = snd ctx.local in
-      let updated_heap_state = List.fold_left (fun heap_state lval -> D.remove lval heap_state) heap_state lvals in
-      (fst ctx.local, updated_heap_state)
-    | _ -> ctx.local
-  
+
+
   (* HELPER FUNCTIONS *)
 
   let get_current_threadid ctx =
@@ -253,5 +243,4 @@ struct
 end
 
 let _ =
-  
-  MCP.register_analysis ~events:[event_function] (module Spec : MCPSpec)
\ No newline at end of file
+  MCP.register_analysis (module Spec : MCPSpec)
\ No newline at end of file
diff --git a/tests/practical/test_file b/tests/practical/test_file
deleted file mode 100644
index 4eae6d8ae4..0000000000
--- a/tests/practical/test_file
+++ /dev/null
@@ -1,16 +0,0 @@
-#include <stdlib.h>
-
-int main() {
-    int *ptr = (int *)malloc(sizeof(int));
-
-    // Access allocated memory
-    *ptr = 42;
-
-    // Free the allocated memory
-    free(ptr);
-
-    // Access the freed memory (use-after-free)
-    int value = *ptr;  // This should trigger a use-after-free warning
-
-    return 0;
-}

From 6834957b1c126c672a513444c74ce7821a6d84a0 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 11 Jan 2024 15:27:44 +0100
Subject: [PATCH 22/62] Revert "region-analysis" (doesn't compile)

This reverts commit 4bc2e6724ffccdc0c3a27a3f0cde7075a364cb87.
---
 src/analyses/region.ml | 17 +----------------
 1 file changed, 1 insertion(+), 16 deletions(-)

diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 916a08e4a4..6d2ae246c3 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -58,21 +58,6 @@ struct
         ls
     | _ -> Queries.Result.top q
 
-    let event ctx e octx =
-      match e with
-      | Events.Invalidate {lvals} ->
-        begin
-          match ctx.local with
-          | `Lifted reg ->
-            let invalidation_set = Lvals.of_list lvals in
-            let updated_reg = RegMap.mapi (fun v r ->
-              if Lvals.mem v invalidation_set then RegPart.top () else r
-            ) reg in
-            `Lifted updated_reg
-          | _ -> ctx.local
-        end
-      | _ -> ctx.local  
-
   module Lvals = SetDomain.Make (Mval.Exp)
   module A =
   struct
@@ -200,4 +185,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis ~events:[Spec.event] (module Spec : MCPSpec)
+  MCP.register_analysis (module Spec : MCPSpec)

From bcfb1729cf5770c04a6c254132b07e33432097b4 Mon Sep 17 00:00:00 2001
From: ge46lup <ge46lup@tum.de>
Date: Thu, 11 Jan 2024 16:41:32 +0100
Subject: [PATCH 23/62] changes in region, useAfterFree and
 taintPartialContexts

---
 src/analyses/region.ml               | 32 +++++++++++++++++-----------
 src/analyses/taintPartialContexts.ml | 12 +++++++++++
 src/analyses/useAfterFree.ml         | 30 ++++++++++++++++++--------
 tests/practical/test_file            | 16 --------------
 4 files changed, 53 insertions(+), 37 deletions(-)
 delete mode 100644 tests/practical/test_file

diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index f789e422f2..c3ad955931 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -82,17 +82,25 @@ struct
   let event ctx e octx =
     match e with
     | Events.Invalidate {lvals} ->
-      begin
-        match ctx.local with
-        | `Lifted reg ->
-          let invalidation_set = Lvals.of_list lvals in
-          let updated_reg = RegMap.mapi (fun v r ->
-            if Lvals.mem v invalidation_set then RegPart.top () else r
-          ) reg in
-          `Lifted updated_reg
-        | _ -> ctx.local
-      end
-    | _ -> ctx.local  
+        begin
+          match ctx.local with
+          | `Lifted reg ->
+            let old_regpart = ctx.global () in
+            let regpart, reg =
+              List.fold_left
+                (fun (regpart_acc, reg_acc) lval ->
+                  Reg.assign_bullet lval (regpart_acc, reg_acc)
+                )
+                (old_regpart, reg)
+                lvals
+            in
+            if not (RegPart.leq regpart old_regpart) then
+              ctx.sideg () regpart;
+            `Lifted reg
+          | _ -> ctx.local
+        end
+      | _ -> ctx.local
+    
 
   let access ctx (a: Queries.access) =
     match a with
@@ -204,4 +212,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis ~events:[Spec.event] (module Spec : MCPSpec)
+  MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index feb9599977..7482023e97 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -103,6 +103,18 @@ struct
 
 end
 
+let event ctx e octx =
+  match e with
+  | Events.Invalidate {lvals} ->
+    (* Handle the Invalidate event and update the tainted set *)
+    List.fold_left (fun acc lval ->
+      Spec.taint_lval ctx lval 
+    ) ctx.local lvals
+   
+  | _ -> ctx.local
+
+
+
 let _ =
   MCP.register_analysis (module Spec : MCPSpec)
 
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 325f1876ca..9888438ae9 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -28,14 +28,7 @@ struct
  
   
   
-  let event_function (ctx: (D.t, G.t, C.t, V.t) ctx) (event: Events.t) : (D.t * D.t) =
-    match event with
-    | Events.Invalidate { lvals } ->
-      (* Remove invalidated or freed heap variables from the heSap state *)
-      let heap_state = snd ctx.local in
-      let updated_heap_state = List.fold_left (fun heap_state lval -> D.remove lval heap_state) heap_state lvals in
-      (fst ctx.local, updated_heap_state)
-    | _ -> ctx.local
+  
   
   (* HELPER FUNCTIONS *)
 
@@ -246,6 +239,25 @@ struct
         | _ -> state
       end
     | _ -> state
+    
+    
+
+    let event ctx e octx =
+      match e with
+      | Events.Invalidate { lvals } ->
+        let updated_heap_state =
+          (*let _, heap_state = ctx.local in*)
+          List.fold_left (fun (stack_state, heap_state) lval ->
+            match lval with
+            | Var var, _ -> (stack_state, HeapVars.remove var heap_state)  
+            | _ -> (stack_state, heap_state)
+            )  ctx.local lvals in
+               updated_heap_state
+      | _ -> ctx.local
+     
+      
+      
+    
 
   let startstate v = D.bot ()
   let exitstate v = D.top ()
@@ -254,4 +266,4 @@ end
 
 let _ =
   
-  MCP.register_analysis ~events:[event_function] (module Spec : MCPSpec)
\ No newline at end of file
+  MCP.register_analysis (module Spec : MCPSpec)
\ No newline at end of file
diff --git a/tests/practical/test_file b/tests/practical/test_file
deleted file mode 100644
index 4eae6d8ae4..0000000000
--- a/tests/practical/test_file
+++ /dev/null
@@ -1,16 +0,0 @@
-#include <stdlib.h>
-
-int main() {
-    int *ptr = (int *)malloc(sizeof(int));
-
-    // Access allocated memory
-    *ptr = 42;
-
-    // Free the allocated memory
-    free(ptr);
-
-    // Access the freed memory (use-after-free)
-    int value = *ptr;  // This should trigger a use-after-free warning
-
-    return 0;
-}

From 31952efdf83b786290f3e6e6b2019a6e4c41ba5f Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 11 Jan 2024 17:24:26 +0100
Subject: [PATCH 24/62] my stuff

---
 src/analyses/accessAnalysis.ml  |  9 +--------
 src/analyses/locksetAnalysis.ml |  7 -------
 src/analyses/memLeak.ml         | 22 ++++++++--------------
 src/analyses/symbLocks.ml       |  7 +++++++
 src/analyses/uninit.ml          | 22 ++++++++++++++++++++++
 5 files changed, 38 insertions(+), 29 deletions(-)

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index 53033640cc..c7624c1262 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -85,14 +85,7 @@ struct
           List.map third asm_in
         | _ -> failwith "transfer function asm called on non-asm edge"
       in
-      let handle_in exp = 
-        match exp with
-        | Cil.Lval lval ->
-          if not (List.mem lval asm_out) then
-            access_one_top ~deref:true ctx Read false (AddrOf lval)
-          else ()
-        | _ -> access_one_top ctx Read false exp
-      in
+      let handle_in exp = access_one_top ~deref:true ctx Read false exp in
       List.iter handle_in asm_in;
       ctx.emit (Events.Invalidate {lvals=asm_out})
 
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 27b93a8fc3..9171fe7c1a 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -67,13 +67,6 @@ struct
       ctx.local (* don't remove non-unique lock *)
     | Events.Unlock l ->
       Arg.remove ctx l (* remove definite lock or none in parallel if ambiguous *)
-    | Events.Invalidate {lvals} ->
-      let locks = locks_of_lvals ctx lvals in
-      let is_held lock = Arg.is_held ctx lock in
-      let locks = List.filter is_held locks in
-      let remove_lock ctx lock = {ctx with local = Arg.remove ctx lock} in
-      let ctx = List.fold_left remove_lock ctx locks in
-      ctx.local
     | _ ->
       ctx.local
 end
diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml
index fa66f2e9cf..72c0febb4d 100644
--- a/src/analyses/memLeak.ml
+++ b/src/analyses/memLeak.ml
@@ -45,17 +45,6 @@ struct
     if f.svar.vname = "main" then check_for_mem_leak ctx;
     ctx.local
 
-  let heapvar_from_ptr_opt ctx ptr = 
-    begin match ctx.ask (Queries.MayPointTo ptr) with
-      | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad = 1 ->
-        (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *)
-        begin match Queries.AD.choose ad with
-          | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> Some v
-          | _ -> None
-        end
-      | _ -> None
-    end
-
   let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t =
     let state = ctx.local in
     let desc = LibraryFunctions.find f in
@@ -70,9 +59,14 @@ struct
         | _ -> state
       end
     | Free ptr ->
-      begin match heapvar_from_ptr_opt ctx ptr with
-        | Some v -> D.remove v state
-        | None -> state
+      begin match ctx.ask (Queries.MayPointTo ptr) with
+        | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad = 1 ->
+          (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *)
+          begin match Queries.AD.choose ad with
+            | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> D.remove v state
+            | _ -> state
+          end
+        | _ -> state
       end
     | Abort ->
       (* An "Abort" special function indicates program exit => need to check for memory leaks *)
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index d8cebf51d2..dad0e4ad54 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -103,6 +103,13 @@ struct
       (* TODO: why doesn't invalidate_exp involve any reachable for deep write? *)
       List.fold_left (fun st e -> invalidate_exp (Analyses.ask_of_ctx ctx) e st) st write_args
 
+  let event ctx e octx =
+    match e with
+    | Events.Invalidate {lvals} ->
+      let ask = Analyses.ask_of_ctx ctx in
+      let invalidate local lval = invalidate_lval ask lval local in
+      List.fold_left invalidate ctx.local lvals
+    | _ -> ctx.local
 
   module A =
   struct
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index f8759d9134..bb2a0afff4 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -7,6 +7,7 @@ module Offs = ValueDomain.Offs
 
 open GoblintCil
 open Analyses
+open GobConfig
 
 module Spec =
 struct
@@ -29,6 +30,11 @@ struct
   let threadspawn ctx 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 access_address (ask: Queries.ask) write lv =
     match ask.f (Queries.MayPointTo (AddrOf lv)) with
     | ad when not (Queries.AD.is_top ad) ->
@@ -223,6 +229,22 @@ struct
     ignore (is_expr_initd (Analyses.ask_of_ctx ctx) rval ctx.local);
     init_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
+  let asm ctx =
+    if not !ignore_asm then
+      let asm_out, asm_in = 
+        match ctx.edge with
+        | ASM (_, asm_out, asm_in, _) ->
+          let third (_, _, x) = x in
+          List.map third asm_out,
+          List.map third asm_in
+        | _ -> failwith "transfer function asm called on non-asm edge"
+      in
+      let handle_in exp = ignore (is_expr_initd (Analyses.ask_of_ctx ctx) exp ctx.local) in
+      List.iter handle_in asm_in;
+      let handle_out local lval = init_lval (Analyses.ask_of_ctx ctx) lval local in
+      List.fold_left handle_out ctx.local asm_out
+    else ctx.local
+
   let branch ctx (exp:exp) (tv:bool) : trans_out =
     ignore (is_expr_initd (Analyses.ask_of_ctx ctx) exp ctx.local);
     ctx.local

From d831e1f891c754d576fb27a066ab8ffb8b78229d Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 11 Jan 2024 19:52:53 +0100
Subject: [PATCH 25/62] init function on malloc_null is never
 called????????????/

---
 src/analyses/accessAnalysis.ml |  4 +++-
 src/analyses/malloc_null.ml    | 19 +++++++++++++++++++
 src/analyses/uninit.ml         |  6 ++++++
 src/analyses/useAfterFree.ml   | 18 +++++++++++++-----
 4 files changed, 41 insertions(+), 6 deletions(-)

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index a752665d4a..b9ed7eabff 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -25,8 +25,10 @@ struct
 
   let collect_local = ref false
   let emit_single_threaded = ref false
+  let ignore_asm = ref true
 
   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 (ModifiedSinceLongjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
@@ -73,7 +75,7 @@ struct
       ctx.local
     end
 
-  let asm_ins_outs ctx =
+  let asm ctx =
     let ins, outs = Analyses.asm_extract_ins_outs ctx in
     let handle_in exp = access_one_top ~deref:true ctx Read false exp in
     List.iter handle_in ins;
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 4d5871cb80..75f0f16ca4 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -6,6 +6,7 @@ module Offs = ValueDomain.Offs
 
 open GoblintCil
 open Analyses
+open GobConfig
 
 module Spec =
 struct
@@ -16,6 +17,12 @@ 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"
+
   (*
     Addr set functions:
   *)
@@ -153,6 +160,18 @@ struct
       D.add (Addr.of_mval mval) ctx.local
     | _ -> 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
+      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;
+      let handle_out lval = warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local (Lval lval) in
+      List.iter handle_out outs;
+    end;
+    ctx.local
+
   let branch ctx (exp:exp) (tv:bool) : D.t =
     warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local exp;
     ctx.local
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index 2ad4eb12c9..da07af7f70 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -7,6 +7,7 @@ module Offs = ValueDomain.Offs
 
 open GoblintCil
 open Analyses
+open GobConfig
 
 module Spec =
 struct
@@ -29,6 +30,11 @@ struct
   let threadspawn ctx 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 access_address (ask: Queries.ask) write lv =
     match ask.f (Queries.MayPointTo (AddrOf lv)) with
     | ad when not (Queries.AD.is_top ad) ->
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index e8f2dac07b..067e68b5ca 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -4,6 +4,7 @@ open GoblintCil
 open Analyses
 open MessageCategory
 open AnalysisStateUtil
+open GobConfig
 
 module AllocaVars = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All alloca() Variables" end)
 module HeapVars = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)
@@ -24,6 +25,11 @@ struct
   module G = ThreadIdToJoinedThreadsMap
   module V = VarinfoV
 
+  let ignore_asm = ref true
+
+  let init _ =
+    ignore_asm := get_bool "asm_is_nop"
+
   let context _ _ = ()
   (* HELPER FUNCTIONS *)
 
@@ -170,11 +176,13 @@ struct
     ctx.local
 
   let asm ctx =
-    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;
-    let handle_in exp = warn_exp_might_contain_freed "asm" ctx exp in
-    List.iter handle_in ins;
+    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;
+      let handle_in exp = warn_exp_might_contain_freed "asm" ctx exp in
+      List.iter handle_in ins;
+    end;
     ctx.local
 
   let return ctx (exp:exp option) (f:fundec) : D.t =

From bb71066e58936bb78779017375a5cea37d4ead05 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 11 Jan 2024 20:11:57 +0100
Subject: [PATCH 26/62] my tests, TODO: add annotations

---
 tests/practical/deadlock.c       | 30 ++++++++++++++++++++++++++++++
 tests/practical/expsplit.c       | 11 +++++++++++
 tests/practical/file-use.c       |  9 +++++++++
 tests/practical/mem-leak.c       |  9 +++++++++
 tests/practical/tmp-special.c    |  7 +++++++
 tests/practical/uninit.c         |  6 ++++++
 tests/practical/use-after-free.c |  7 +++++++
 tests/practical/var-eq.c         |  6 ++++++
 8 files changed, 85 insertions(+)
 create mode 100644 tests/practical/deadlock.c
 create mode 100644 tests/practical/expsplit.c
 create mode 100644 tests/practical/file-use.c
 create mode 100644 tests/practical/mem-leak.c
 create mode 100644 tests/practical/tmp-special.c
 create mode 100644 tests/practical/uninit.c
 create mode 100644 tests/practical/use-after-free.c
 create mode 100644 tests/practical/var-eq.c

diff --git a/tests/practical/deadlock.c b/tests/practical/deadlock.c
new file mode 100644
index 0000000000..2f24415d8f
--- /dev/null
+++ b/tests/practical/deadlock.c
@@ -0,0 +1,30 @@
+#include <unistd.h>
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_mutex_t lock_a;
+pthread_mutex_t lock_b;
+
+void *proc_a(void *arg) {
+    pthread_mutex_lock(&lock_a);
+    sleep(1);
+    pthread_mutex_lock(&lock_b);
+    pthread_exit(NULL);
+}
+
+void *proc_b(void *arg) {
+    pthread_mutex_lock(&lock_b);
+    sleep(1);
+    pthread_mutex_lock(&lock_a);
+    return NULL;
+}
+
+int main(void) {
+    pthread_t a, b;
+    pthread_create(&a, NULL, proc_a, NULL);
+    proc_b(NULL);
+    int x, y;
+    asm ("nop" : "=g" (lock_a), "=x" (x));
+    asm ("nop" : "=g" (lock_a), "=x" (x));
+    puts("no deadlock!");
+}
diff --git a/tests/practical/expsplit.c b/tests/practical/expsplit.c
new file mode 100644
index 0000000000..09462c0fdd
--- /dev/null
+++ b/tests/practical/expsplit.c
@@ -0,0 +1,11 @@
+#include <goblint.h>
+
+int main(void) {
+  int r, x;
+  __goblint_split_begin(x);
+  x = r ? 1 : 0;
+  asm("nop" : "=x" (x), "=x" (r));
+  __goblint_check(x == 0 || x == 1);
+  __goblint_split_end(x);
+  __goblint_check(x == 0 || x == 1);
+}
diff --git a/tests/practical/file-use.c b/tests/practical/file-use.c
new file mode 100644
index 0000000000..0e5693172b
--- /dev/null
+++ b/tests/practical/file-use.c
@@ -0,0 +1,9 @@
+#include <stdio.h>
+
+int main(void) {
+  FILE *f = fopen("file-use.c", "r");
+  //int x;
+  //asm ("nop" : "=g" (f), "=g" (x));
+  fclose(f);
+  return 0;
+}
diff --git a/tests/practical/mem-leak.c b/tests/practical/mem-leak.c
new file mode 100644
index 0000000000..f67b9f53e6
--- /dev/null
+++ b/tests/practical/mem-leak.c
@@ -0,0 +1,9 @@
+#include <stdlib.h>
+
+int main(void) {
+  char *x = malloc(64);
+  char *y = x;
+  asm ("nop" : "=x" (*x));
+  free(y);
+  return 0;
+}
diff --git a/tests/practical/tmp-special.c b/tests/practical/tmp-special.c
new file mode 100644
index 0000000000..0195ef6d5c
--- /dev/null
+++ b/tests/practical/tmp-special.c
@@ -0,0 +1,7 @@
+#include <math.h>
+
+int main(void) {
+  int x = floor(0.8);
+  asm ("nop" : "=x" (x));
+  return x;
+}
diff --git a/tests/practical/uninit.c b/tests/practical/uninit.c
new file mode 100644
index 0000000000..ad379f1634
--- /dev/null
+++ b/tests/practical/uninit.c
@@ -0,0 +1,6 @@
+int main(void) {
+  int x;
+  int y;
+  asm ("nop" : "=x" (y) : "x" (x));
+  return y;
+}
diff --git a/tests/practical/use-after-free.c b/tests/practical/use-after-free.c
new file mode 100644
index 0000000000..77fc912313
--- /dev/null
+++ b/tests/practical/use-after-free.c
@@ -0,0 +1,7 @@
+#include <stdlib.h>
+
+int main(void) {
+  int *x = malloc(16);
+  free(x);
+  asm ("nop" : "=x" (*x));
+}
diff --git a/tests/practical/var-eq.c b/tests/practical/var-eq.c
new file mode 100644
index 0000000000..2f8d529984
--- /dev/null
+++ b/tests/practical/var-eq.c
@@ -0,0 +1,6 @@
+int main(void) {
+    int x = 0;
+    int y = x;
+    asm ("mov $1, %0" : "=x" (x));
+    return 0;
+}

From e22323cf93267c01145fea920a44810b29d90b16 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 11 Jan 2024 20:24:33 +0100
Subject: [PATCH 27/62] bugfix

---
 src/analyses/accessAnalysis.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index b9ed7eabff..d111456484 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -77,8 +77,10 @@ struct
 
   let asm ctx =
     let ins, outs = Analyses.asm_extract_ins_outs ctx in
-    let handle_in exp = access_one_top ~deref:true ctx Read false exp 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 ~deref:true ctx Write false (AddrOf lval) in
+    List.iter handle_out outs;
     ctx.emit (Events.Invalidate {lvals=outs})
 
   let branch ctx exp tv : D.t =

From bb9582b966708751fb23490db40672b3735c7636 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 11 Jan 2024 20:38:18 +0100
Subject: [PATCH 28/62] bugfix

---
 src/analyses/accessAnalysis.ml | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index d111456484..ef276ec44f 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -76,12 +76,16 @@ struct
     end
 
   let asm ctx =
-    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 ~deref:true ctx Write false (AddrOf lval) in
-    List.iter handle_out outs;
-    ctx.emit (Events.Invalidate {lvals=outs})
+    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 ~deref:true ctx Write false (AddrOf lval) in
+      List.iter handle_out outs;
+      ctx.emit (Events.Invalidate {lvals=outs})
+    end;
+    ctx.local
+
 
   let branch ctx exp tv : D.t =
     access_one_top ctx Read false exp;

From 134b0323672ddc806163c04f67460c3b79f4f4d9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Konrad=20G=C3=B6=C3=9Fmann?= <konrad.goessmann@tum.de>
Date: Fri, 12 Jan 2024 01:37:07 +0100
Subject: [PATCH 29/62] Modifications of Variables by assembly between setjmp
 and longjmp are now recognized.

---
 src/analyses/modifiedSinceLongjmp.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml
index 5dae8748cb..0dcfb78893 100644
--- a/src/analyses/modifiedSinceLongjmp.ml
+++ b/src/analyses/modifiedSinceLongjmp.ml
@@ -69,6 +69,14 @@ 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

From f13782465496cb70deb4eb90f487d0c4420529cd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Konrad=20G=C3=B6=C3=9Fmann?= <konrad.goessmann@tum.de>
Date: Fri, 12 Jan 2024 03:56:54 +0100
Subject: [PATCH 30/62] CondVar assumptions about lvals are dropped after
 clobber by asm.

---
 src/analyses/condVars.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 04b148dd02..c95f44dbea 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -101,6 +101,15 @@ struct
       of_expr true e >? of_lval >? of_clval |? Queries.Result.top q
     | _ -> Queries.Result.top q
 
+  let event ctx event octx = 
+    match event with
+    | Events.Invalidate {lvals} -> 
+      let mpts = List.map (fun lval -> mayPointTo ctx (AddrOf lval)) lvals in
+      let remove_mpt d mpt =
+        List.fold_left (fun d (v,o as k) -> D.remove k d |> D.remove_var v) d mpt in
+      List.fold_left remove_mpt ctx.local mpts
+    | _ -> ctx.local
+  
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
     (* remove all keys lval may point to, and all exprs that contain the variables (TODO precision) *)

From 5f7a314b80472e0c42b73dad5a0b4c5acf30f13a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Konrad=20G=C3=B6=C3=9Fmann?= <konrad.goessmann@tum.de>
Date: Fri, 12 Jan 2024 03:56:54 +0100
Subject: [PATCH 31/62] CondVar assumptions about lvals are dropped after
 clobber by asm.

---
 src/analyses/condVars.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 04b148dd02..c95f44dbea 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -101,6 +101,15 @@ struct
       of_expr true e >? of_lval >? of_clval |? Queries.Result.top q
     | _ -> Queries.Result.top q
 
+  let event ctx event octx = 
+    match event with
+    | Events.Invalidate {lvals} -> 
+      let mpts = List.map (fun lval -> mayPointTo ctx (AddrOf lval)) lvals in
+      let remove_mpt d mpt =
+        List.fold_left (fun d (v,o as k) -> D.remove k d |> D.remove_var v) d mpt in
+      List.fold_left remove_mpt ctx.local mpts
+    | _ -> ctx.local
+  
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
     (* remove all keys lval may point to, and all exprs that contain the variables (TODO precision) *)

From 91d85f33baa851149a18b28e29015be44e4bcde0 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Fri, 12 Jan 2024 12:50:07 +0100
Subject: [PATCH 32/62] moved invalidate emit to base

---
 src/analyses/accessAnalysis.ml | 1 -
 src/analyses/base.ml           | 5 +++++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index 68c9ffb8f9..9bbf6a8289 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -82,7 +82,6 @@ struct
       List.iter handle_in ins;
       let handle_out lval = access_one_top ~deref:true ctx Write false (AddrOf lval) in
       List.iter handle_out outs;
-      ctx.emit (Events.Invalidate {lvals=outs})
     end;
     ctx.local
 
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 33b6cdc24d..1f782a1a39 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2890,6 +2890,11 @@ struct
     in
     D.join ctx.local e_d'
 
+  let asm ctx = 
+    let _, outs = Analyses.asm_extract_ins_outs ctx in
+    ctx.emit (Events.Invalidate {lvals=outs});
+    ctx.local
+
   let event ctx e octx =
     let st: store = ctx.local in
     match e with

From d2d947448dae4069139a2daba9bdfcf6b8604199 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Fri, 12 Jan 2024 13:40:08 +0100
Subject: [PATCH 33/62] maybe like this?

---
 goblint.opam | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/goblint.opam b/goblint.opam
index 7a75a1fb45..565c660718 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -77,7 +77,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#d2760bacfbfdb25a374254de44f2ff1cb5f42abd" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/N0W0RK/goblint-cil#7e5435dbebc63b0bcda6bc84fe874a2e9187c3c1" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]

From 937517608757f621744e2d6a31d05dcdd22f62a6 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Fri, 12 Jan 2024 13:46:40 +0100
Subject: [PATCH 34/62] I am retarded

---
 goblint.opam | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/goblint.opam b/goblint.opam
index 565c660718..a2adfc3379 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -77,7 +77,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/N0W0RK/goblint-cil#7e5435dbebc63b0bcda6bc84fe874a2e9187c3c1" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/N0W0RK/goblint-cil.git#7e5435dbebc63b0bcda6bc84fe874a2e9187c3c1" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]

From eb4151392585c3be3c2aae87aa0f4d174d4ab96e Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Fri, 12 Jan 2024 15:20:17 +0100
Subject: [PATCH 35/62] followed orders

---
 goblint.opam.locked | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/goblint.opam.locked b/goblint.opam.locked
index b0a1c9ef20..afd42ba532 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -131,6 +131,10 @@ post-messages: [
 ]
 # TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
 pin-depends: [
+  [
+    "goblint-cil.2.0.3"
+    "git+https://github.com/N0W0RK/goblint-cil.git#7e5435dbebc63b0bcda6bc84fe874a2e9187c3c1" 
+  ]
   [
     "ppx_deriving.5.2.1"
     "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"

From 90946cd1106646e487df12801467ed2e5c3dfeb2 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Sun, 14 Jan 2024 12:37:50 +0100
Subject: [PATCH 36/62] can one also point to latest commit?

---
 goblint.opam        | 2 +-
 goblint.opam.locked | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/goblint.opam b/goblint.opam
index a2adfc3379..d1f7469f25 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -77,7 +77,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/N0W0RK/goblint-cil.git#7e5435dbebc63b0bcda6bc84fe874a2e9187c3c1" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/N0W0RK/goblint-cil.git#a339860985a17511723917e36d2745289334b463" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]
diff --git a/goblint.opam.locked b/goblint.opam.locked
index afd42ba532..67a541df2d 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -133,7 +133,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.3"
-    "git+https://github.com/N0W0RK/goblint-cil.git#7e5435dbebc63b0bcda6bc84fe874a2e9187c3c1" 
+    "git+https://github.com/N0W0RK/goblint-cil.git#a339860985a17511723917e36d2745289334b463" 
   ]
   [
     "ppx_deriving.5.2.1"

From b55366ceaad04d4be0d5c5fb7ae393bab360b49b Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Mon, 15 Jan 2024 11:06:29 +0100
Subject: [PATCH 37/62] maybe

---
 goblint.opam        | 2 +-
 goblint.opam.locked | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/goblint.opam b/goblint.opam
index d1f7469f25..871ac17739 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -77,7 +77,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/N0W0RK/goblint-cil.git#a339860985a17511723917e36d2745289334b463" ]
+  [ "goblint-cil.2.0.3" "git+https://github.com/N0W0RK/goblint-cil.git#second_try" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 67a541df2d..d66084af78 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -133,7 +133,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.3"
-    "git+https://github.com/N0W0RK/goblint-cil.git#a339860985a17511723917e36d2745289334b463" 
+    "git+https://github.com/N0W0RK/goblint-cil.git#second_try" 
   ]
   [
     "ppx_deriving.5.2.1"

From a75b93119a704b6a42dcf92049059612ad68513a Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Wed, 17 Jan 2024 09:28:08 +0100
Subject: [PATCH 38/62] forgot to pull

---
 src/analyses/accessAnalysis.ml |  2 +-
 src/analyses/base.ml           |  3 +--
 src/analyses/mallocFresh.ml    | 23 +++++++----------------
 src/goblint.ml                 |  2 +-
 4 files changed, 10 insertions(+), 20 deletions(-)

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index 9bbf6a8289..c9f2935cce 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -80,7 +80,7 @@ struct
       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 ~deref:true ctx Write false (AddrOf lval) in
+      let handle_out lval = access_one_top ctx Write false (AddrOf lval) in
       List.iter handle_out outs;
     end;
     ctx.local
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 1f782a1a39..185f8e7bcc 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1229,9 +1229,8 @@ struct
             | JmpBuf (x, copied, invalid) ->
               if copied then
                 M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e;
-              (* M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a was modified by inline assembly. This is may lead to Undefined Behavior." d_exp e; *)
               if invalid then
-                M.warn ~category:(Behavior (Undefined Other)) "The jump target %a may have been altered in an inline assembly block." d_exp e;
+                M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a was modified by inline assembly. This is may lead to Undefined Behavior." d_exp e;
               x
             | Top
             | Bot ->
diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index 227c497f9d..0bc0c0e4c3 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -29,22 +29,13 @@ struct
   let assign ctx lval rval =
     assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
-    let is_relevant_variable v =
-      (* Check if the variable is a global variable *)
-      v.vglob
-    
-    let event ctx e octx =
-        match e with
-        | Events.Invalidate {lvals} ->
-          (* Perform invalidation for mallocFresh analysis *)
-          let updated_locals = List.fold_left (fun acc lval ->
-            (* Check if lval is relevant to mallocFresh analysis and update the domain accordingly *)
-            match lval with
-            | (Var v, _) when is_relevant_variable v -> D.remove v acc
-            | _ -> acc
-          ) ctx.local lvals in
-          updated_locals
-        | _ -> ctx.local  
+  let event ctx e octx =
+    match e with
+    | Events.Invalidate {lvals} ->
+      let ask = Analyses.ask_of_ctx ctx in
+      let handle_lval local lval = assign_lval ask lval local in
+      List.fold_left handle_lval ctx.local lvals
+    | _ -> ctx.local
 
   let combine_env ctx lval fexp f args fc au f_ask =
     ctx.local (* keep local as opposed to IdentitySpec *)
diff --git a/src/goblint.ml b/src/goblint.ml
index 4bef41f370..25e809f9e9 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -61,7 +61,7 @@ let main () =
       (* This is run independant of the autotuner being enabled or not be sound for programs with longjmp *)
       AutoTune.activateLongjmpAnalysesWhenRequired ();
       if get_bool "ana.autotune.enabled" then AutoTune.chooseConfig file;
-      file |> do_analyze changeInfo; 
+      file |> do_analyze changeInfo;
       do_html_output ();
       do_gobview file;
       do_stats ();

From cb09957aa1a525dafbd2e3a64f5c8bd04b567fc7 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Wed, 17 Jan 2024 10:20:11 +0100
Subject: [PATCH 39/62] todo: starting at valueDomain.ml (email), wtf should I
 do in cfgtools

---
 src/analyses/accessAnalysis.ml      |  8 ++++----
 src/analyses/base.ml                |  8 ++++++--
 src/analyses/malloc_null.ml         | 10 ++--------
 src/analyses/modifiedSinceSetjmp.ml |  8 --------
 src/analyses/uninit.ml              | 17 ++++++++---------
 src/analyses/useAfterFree.ml        |  7 ++-----
 src/common/framework/cfgTools.ml    | 24 ++++++++++++------------
 7 files changed, 34 insertions(+), 48 deletions(-)

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index c9f2935cce..f3cd3870a6 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/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
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 185f8e7bcc..a3127d4a71 100644
--- a/src/analyses/base.ml
+++ b/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 =
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 22c5d8e35b..b306dbfcce 100644
--- a/src/analyses/malloc_null.ml
+++ b/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;
diff --git a/src/analyses/modifiedSinceSetjmp.ml b/src/analyses/modifiedSinceSetjmp.ml
index 512276915a..93e55b2a17 100644
--- a/src/analyses/modifiedSinceSetjmp.ml
+++ b/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
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index 9146d90923..32fa5da0ec 100644
--- a/src/analyses/uninit.ml
+++ b/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);
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index f20572512c..b62a5e46af 100644
--- a/src/analyses/useAfterFree.ml
+++ b/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;
diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml
index 63407126bc..1216c4e6f7 100644
--- a/src/common/framework/cfgTools.ml
+++ b/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 _ ->

From 2570bc6ad4beffb37c192051e71eb90784164f68 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Wed, 17 Jan 2024 14:33:48 +0100
Subject: [PATCH 40/62] went through everything

---
 src/cdomain/value/cdomains/valueDomain.ml |  2 +-
 src/common/framework/edge.ml              |  3 ++-
 src/config/options.schema.json            |  2 +-
 src/framework/constraints.ml              | 16 ++++++++--------
 src/maingoblint.ml                        |  2 +-
 5 files changed, 13 insertions(+), 12 deletions(-)

diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml
index 363900180e..4729424221 100644
--- a/src/cdomain/value/cdomains/valueDomain.ml
+++ b/src/cdomain/value/cdomains/valueDomain.ml
@@ -725,7 +725,7 @@ struct
       Array (CArrays.set ask n (array_idx_top) v)
     |                 t , Blob n       -> Blob (Blobs.invalidate_value ask t n)
     |                 _ , Thread tid   -> Thread (Threads.join (Threads.top ()) tid)
-    |                 _ , JmpBuf (b, c, _)     -> JmpBuf(b, c, true) (* TODO: no top jmpbuf *)
+    |                 _ , JmpBuf (b, c, _)     -> JmpBuf(b, c, true)
     | _, Bot -> Bot (* Leave uninitialized value (from malloc) alone in free to avoid trashing everything. TODO: sound? *)
     |                 t , _             -> top_value t
 
diff --git a/src/common/framework/edge.ml b/src/common/framework/edge.ml
index fc918c80db..8e66177bcb 100644
--- a/src/common/framework/edge.ml
+++ b/src/common/framework/edge.ml
@@ -23,7 +23,8 @@ type t =
   (** The true-branch or false-branch of a conditional exp *)
   | ASM of string list * asm_out * asm_in * bool
   (** Inline assembly statements, and the annotations for output and input
-    * variables. The last field is a flag that indicates if this is a duplicated edge. *)
+    * variables. The last field is a flag that indicates if this is an edge that
+    * was inserted because of asm goto labels. *)
   | VDecl of CilType.Varinfo.t
   (** VDecl edge for the variable in varinfo. Whether such an edge is there for all
     * local variables or only when it is not possible to pull the declaration up, is
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index d973b7b4f0..fa01e7c655 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -19,7 +19,7 @@
     },
     "asm_is_nop": {
       "title": "asm_is_nop",
-      "description": "treat asm statements as nop",
+      "description": "Treat assembly statements as NOOP",
       "type": "boolean",
       "default": true
     },
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index e44c5a39e4..69b0023866 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -775,14 +775,14 @@ struct
 
   let tf var getl sidel getg sideg prev_node edge d =
     begin match edge with
-      | Assign (lv,rv) -> tf_assign var edge prev_node lv rv
-      | VDecl (v)      -> tf_vdecl var edge prev_node v
-      | Proc (r,f,ars) -> tf_proc var edge prev_node r f ars
-      | Entry f        -> tf_entry var edge prev_node f
-      | Ret (r,fd)     -> tf_ret var edge prev_node r fd
-      | Test (p,b)     -> tf_test var edge prev_node p b
-      | ASM (_, _, _,_)  -> tf_asm var edge prev_node (* TODO: use ASM fields for something? *)
-      | Skip           -> tf_skip var edge prev_node
+      | Assign (lv,rv)  -> tf_assign var edge prev_node lv rv
+      | VDecl (v)       -> tf_vdecl var edge prev_node v
+      | Proc (r,f,ars)  -> tf_proc var edge prev_node r f ars
+      | Entry f         -> tf_entry var edge prev_node f
+      | Ret (r,fd)      -> tf_ret var edge prev_node r fd
+      | Test (p,b)      -> tf_test var edge prev_node p b
+      | ASM (_, _, _,_) -> tf_asm var edge prev_node (* TODO: use ASM fields for something? *)
+      | Skip            -> tf_skip var edge prev_node
     end getl sidel getg sideg d
 
   type Goblint_backtrace.mark += TfLocation of location
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 4c98c9c6e2..cc7bfc26c1 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -573,7 +573,7 @@ let do_analyze change_info merged_AST =
         (* Cilfacade.current_file := ast'; *)
     in
 
-    Timing.wrap "analysis" (control_analyze merged_AST) funs 
+    Timing.wrap "analysis" (control_analyze merged_AST) funs
   )
 
 let do_html_output () =

From f3e582bcf139c9a8f0c845b61996fb2721c0b130 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Konrad=20G=C3=B6=C3=9Fmann?= <konrad.goessmann@tum.de>
Date: Tue, 23 Jan 2024 01:54:14 +0100
Subject: [PATCH 41/62] Adds initial regression tests

---
 .../79-assembly/01-assembly-invalidate.c       | 12 ++++++++++++
 .../79-assembly/02-assembly-precision.c        | 18 ++++++++++++++++++
 .../regression/79-assembly/57-jmpbuf-invalid.c | 14 ++++++++++++++
 3 files changed, 44 insertions(+)
 create mode 100644 tests/regression/79-assembly/01-assembly-invalidate.c
 create mode 100644 tests/regression/79-assembly/02-assembly-precision.c
 create mode 100644 tests/regression/79-assembly/57-jmpbuf-invalid.c

diff --git a/tests/regression/79-assembly/01-assembly-invalidate.c b/tests/regression/79-assembly/01-assembly-invalidate.c
new file mode 100644
index 0000000000..7507a8075b
--- /dev/null
+++ b/tests/regression/79-assembly/01-assembly-invalidate.c
@@ -0,0 +1,12 @@
+// PARAM: --set asm_is_nop false
+
+#include <goblint.h>
+
+int main(void) {
+
+    int v = 0;
+
+    __asm__("nop": "=x"(v)); 
+
+    __goblint_assert(v==0); //UNKNOWN
+}
\ No newline at end of file
diff --git a/tests/regression/79-assembly/02-assembly-precision.c b/tests/regression/79-assembly/02-assembly-precision.c
new file mode 100644
index 0000000000..4b318a7cf3
--- /dev/null
+++ b/tests/regression/79-assembly/02-assembly-precision.c
@@ -0,0 +1,18 @@
+// PARAM: --set asm_is_nop false
+
+#include <goblint.h>
+
+int main(void) {
+
+    int r;
+    int v;
+
+    __asm__ goto ("nop": : : : test);
+
+    v = 0;
+
+    test:
+
+    __goblint_assert(v == 0); //UNKNOWN
+
+}
\ No newline at end of file
diff --git a/tests/regression/79-assembly/57-jmpbuf-invalid.c b/tests/regression/79-assembly/57-jmpbuf-invalid.c
new file mode 100644
index 0000000000..5541e706e3
--- /dev/null
+++ b/tests/regression/79-assembly/57-jmpbuf-invalid.c
@@ -0,0 +1,14 @@
+// PARAM: --set asm_is_nop false
+#include <setjmp.h>
+
+jmp_buf buf;
+
+int main(void) {
+
+    if (!setjmp(buf)) {
+
+        __asm__("nop" : "=m"(buf));
+
+        longjmp(buf, 1); //WARN
+    }
+}
\ No newline at end of file

From f6df1c52773d1002b5989a80b89a0ce8f834b14e Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 25 Jan 2024 08:32:11 +0100
Subject: [PATCH 42/62] to pull

---
 tests/practical/deadlock.c | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tests/practical/deadlock.c b/tests/practical/deadlock.c
index 2f24415d8f..5223caa0ed 100644
--- a/tests/practical/deadlock.c
+++ b/tests/practical/deadlock.c
@@ -25,6 +25,5 @@ int main(void) {
     proc_b(NULL);
     int x, y;
     asm ("nop" : "=g" (lock_a), "=x" (x));
-    asm ("nop" : "=g" (lock_a), "=x" (x));
     puts("no deadlock!");
 }

From a3bd48a3571c08ffa1eb1a2bec16b4ebb63499cf Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 25 Jan 2024 09:16:32 +0100
Subject: [PATCH 43/62] tests

---
 src/analyses/accessAnalysis.ml                |  5 +--
 src/analyses/base.ml                          |  6 ++--
 src/analyses/malloc_null.ml                   |  7 ++--
 src/analyses/uninit.ml                        |  7 ++--
 src/analyses/useAfterFree.ml                  |  7 ++--
 src/common/framework/cfgTools.ml              | 19 +++++-----
 .../79-assembly/100-invalidate-asm.c          |  9 +++++
 .../regression/79-assembly/28-asm_deadlock.c  | 35 +++++++++++++++++++
 .../regression/79-assembly/32-asm-mem-leak.c  | 23 ++++++++++++
 9 files changed, 98 insertions(+), 20 deletions(-)
 create mode 100644 tests/regression/79-assembly/100-invalidate-asm.c
 create mode 100644 tests/regression/79-assembly/28-asm_deadlock.c
 create mode 100644 tests/regression/79-assembly/32-asm-mem-leak.c

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index f3cd3870a6..327feb8d62 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -25,9 +25,10 @@ struct
 
   let collect_local = ref false
   let emit_single_threaded = ref false
-  let ignore_asm = get_bool "asm_is_nop"
+  let ignore_asm = ref true
 
   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
@@ -75,7 +76,7 @@ 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;
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index a3127d4a71..68e4489383 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -82,6 +82,7 @@ struct
   let name () = "base"
   let startstate v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
   let exitstate  v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
+  let ignore_asm = ref true
 
   (**************************************************************************
    * Helpers
@@ -160,6 +161,7 @@ struct
     end;
     return_varstore := Cilfacade.create_var @@ makeVarinfo false "RETURN" voidType;
     longjmp_return := Cilfacade.create_var @@ makeVarinfo false "LONGJMP_RETURN" intType;
+    ignore_asm := get_bool "asm_is_nop";
     Priv.init ()
 
   let finalize () =
@@ -2889,10 +2891,8 @@ struct
     in
     D.join ctx.local e_d'
 
-  let ignore_asm = get_bool "asm_is_nop"
-
   let asm ctx = 
-    if not ignore_asm then begin
+    if not !ignore_asm then begin
       let _, outs = Analyses.asm_extract_ins_outs ctx in
       ctx.emit (Events.Invalidate {lvals=outs});
     end;
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index b306dbfcce..588cefc529 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -17,7 +17,10 @@ struct
   module C = ValueDomain.AddrSetDomain
   module P = IdentityP (D)
 
-  let ignore_asm = get_bool "asm_is_nop"
+  let ignore_asm = ref true
+
+  let init _ =
+    ignore_asm := get_bool "asm_is_nop"
 
   (*
     Addr set functions:
@@ -157,7 +160,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_in exp = warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local exp in
       List.iter handle_in ins;
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index 32fa5da0ec..84536e6bf8 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -30,7 +30,10 @@ struct
   let threadspawn ctx ~multiple lval f args fctx = ctx.local
   let exitstate  v : D.t = D.empty ()
 
-  let ignore_asm = get_bool "asm_is_nop"
+  let ignore_asm = ref true
+
+  let init _ =
+    ignore_asm := get_bool "asm_is_nop"
 
   let access_address (ask: Queries.ask) write lv =
     match ask.f (Queries.MayPointTo (AddrOf lv)) with
@@ -227,7 +230,7 @@ struct
     init_lval (Analyses.ask_of_ctx ctx) lval 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_in exp = ignore (is_expr_initd (Analyses.ask_of_ctx ctx) exp ctx.local) in
       List.iter handle_in ins;
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index b62a5e46af..f20572512c 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -25,7 +25,10 @@ struct
   module G = ThreadIdToJoinedThreadsMap
   module V = VarinfoV
 
-  let ignore_asm = get_bool "asm_is_nop"
+  let ignore_asm = ref true
+
+  let init _ =
+    ignore_asm := get_bool "asm_is_nop"
 
   let context _ _ = ()
   (* HELPER FUNCTIONS *)
@@ -173,7 +176,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;
diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml
index 1216c4e6f7..216ed40965 100644
--- a/src/common/framework/cfgTools.ml
+++ b/src/common/framework/cfgTools.ml
@@ -379,15 +379,16 @@ let createCFG (file: file) =
               | [] -> failwith "MyCFG.createCFG: 0 Asm succ"
               | [succ, skippedStatements] -> begin
                 addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, false)) (Statement succ);
-                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;
+                if not (get_bool "asm_is_nop") then
+                  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"
             end
diff --git a/tests/regression/79-assembly/100-invalidate-asm.c b/tests/regression/79-assembly/100-invalidate-asm.c
new file mode 100644
index 0000000000..4e53a8163d
--- /dev/null
+++ b/tests/regression/79-assembly/100-invalidate-asm.c
@@ -0,0 +1,9 @@
+//PARAM: --disable asm_is_nop
+#include <goblint.h>
+
+int main(void) {
+  int x = 0;
+  asm ("nop" : "=x" (x));
+  __goblint_check(x == 0); //WARN
+  return 0;
+}
diff --git a/tests/regression/79-assembly/28-asm_deadlock.c b/tests/regression/79-assembly/28-asm_deadlock.c
new file mode 100644
index 0000000000..2003217713
--- /dev/null
+++ b/tests/regression/79-assembly/28-asm_deadlock.c
@@ -0,0 +1,35 @@
+//PARAM: --set ana.activated[+] deadlock --disable asm_is_nop
+#include <unistd.h>
+#include <pthread.h>
+#include <stdio.h>
+#include <goblint.h>
+
+pthread_mutex_t lock_a;
+pthread_mutex_t lock_b;
+
+extern __goblint_unknown(void*);
+
+void *proc_a(void *arg) {
+    asm ("nop" : "=g" (lock_a));
+    __goblint_unknown(&lock_a);
+    pthread_mutex_lock(&lock_a);
+    sleep(1);
+    pthread_mutex_lock(&lock_b);
+    pthread_exit(NULL);
+}
+
+void *proc_b(void *arg) {
+    pthread_mutex_lock(&lock_b);
+    sleep(1);
+    pthread_mutex_lock(&lock_a);
+    return NULL;
+}
+
+int main(void) {
+    int x;
+    pthread_t a, b;
+    pthread_create(&a, NULL, proc_a, NULL);
+    proc_b(NULL);
+    // this will remove lock_a from must_lockset
+    puts("no deadlock!");
+}
diff --git a/tests/regression/79-assembly/32-asm-mem-leak.c b/tests/regression/79-assembly/32-asm-mem-leak.c
new file mode 100644
index 0000000000..9572a7e842
--- /dev/null
+++ b/tests/regression/79-assembly/32-asm-mem-leak.c
@@ -0,0 +1,23 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --disable asm_is_nop
+#include <stdlib.h>
+
+void ok(void) {
+  char *x = malloc(64);
+  char *y = x;
+  asm ("nop" : "=x" (x));
+  free(y);
+  return; //NOWARN
+}
+
+void not_ok(void) {
+  char *x = malloc(64);
+  asm ("nop" : "=x" (x));
+  free(x);
+  return; //WARN
+}
+
+int main(void) {
+  ok();
+  not_ok();
+  return 0;
+}

From 7b95fcd482eabe892237a2af182ccf90e1cd3fca Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 25 Jan 2024 09:33:10 +0100
Subject: [PATCH 44/62] expsplit-test

---
 .../{practical/expsplit.c => regression/07-asm-exp-split.c} | 3 ++-
 tests/regression/79-assembly/28-asm_deadlock.c              | 6 +-----
 2 files changed, 3 insertions(+), 6 deletions(-)
 rename tests/{practical/expsplit.c => regression/07-asm-exp-split.c} (60%)

diff --git a/tests/practical/expsplit.c b/tests/regression/07-asm-exp-split.c
similarity index 60%
rename from tests/practical/expsplit.c
rename to tests/regression/07-asm-exp-split.c
index 09462c0fdd..75ee44f693 100644
--- a/tests/practical/expsplit.c
+++ b/tests/regression/07-asm-exp-split.c
@@ -1,3 +1,4 @@
+// PARAM: --set ana.activated[+] expsplit --disable asm_is_nop
 #include <goblint.h>
 
 int main(void) {
@@ -7,5 +8,5 @@ int main(void) {
   asm("nop" : "=x" (x), "=x" (r));
   __goblint_check(x == 0 || x == 1);
   __goblint_split_end(x);
-  __goblint_check(x == 0 || x == 1);
+  __goblint_check(x == 0 || x == 1); // UNKNOWN (intentionally)
 }
diff --git a/tests/regression/79-assembly/28-asm_deadlock.c b/tests/regression/79-assembly/28-asm_deadlock.c
index 2003217713..82cad87968 100644
--- a/tests/regression/79-assembly/28-asm_deadlock.c
+++ b/tests/regression/79-assembly/28-asm_deadlock.c
@@ -2,17 +2,13 @@
 #include <unistd.h>
 #include <pthread.h>
 #include <stdio.h>
-#include <goblint.h>
 
 pthread_mutex_t lock_a;
 pthread_mutex_t lock_b;
 
-extern __goblint_unknown(void*);
-
 void *proc_a(void *arg) {
-    asm ("nop" : "=g" (lock_a));
-    __goblint_unknown(&lock_a);
     pthread_mutex_lock(&lock_a);
+    asm ("nop" : "=g" (lock_a));
     sleep(1);
     pthread_mutex_lock(&lock_b);
     pthread_exit(NULL);

From 258ed141098c3453e9472e0c412d36a92e3f939c Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 25 Jan 2024 09:34:52 +0100
Subject: [PATCH 45/62] ups

---
 tests/regression/{ => 79-assembly}/07-asm-exp-split.c | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename tests/regression/{ => 79-assembly}/07-asm-exp-split.c (100%)

diff --git a/tests/regression/07-asm-exp-split.c b/tests/regression/79-assembly/07-asm-exp-split.c
similarity index 100%
rename from tests/regression/07-asm-exp-split.c
rename to tests/regression/79-assembly/07-asm-exp-split.c

From c7b4256b499e9dd2393c59c6c557a63d652230b9 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 25 Jan 2024 09:51:06 +0100
Subject: [PATCH 46/62] use-after-free-test

---
 tests/practical/use-after-free.c                     |  7 -------
 tests/regression/79-assembly/03-asm-use-after-free.c | 11 +++++++++++
 2 files changed, 11 insertions(+), 7 deletions(-)
 delete mode 100644 tests/practical/use-after-free.c
 create mode 100644 tests/regression/79-assembly/03-asm-use-after-free.c

diff --git a/tests/practical/use-after-free.c b/tests/practical/use-after-free.c
deleted file mode 100644
index 77fc912313..0000000000
--- a/tests/practical/use-after-free.c
+++ /dev/null
@@ -1,7 +0,0 @@
-#include <stdlib.h>
-
-int main(void) {
-  int *x = malloc(16);
-  free(x);
-  asm ("nop" : "=x" (*x));
-}
diff --git a/tests/regression/79-assembly/03-asm-use-after-free.c b/tests/regression/79-assembly/03-asm-use-after-free.c
new file mode 100644
index 0000000000..47d57f92f6
--- /dev/null
+++ b/tests/regression/79-assembly/03-asm-use-after-free.c
@@ -0,0 +1,11 @@
+//PARAM: --set ana.activated[+] useAfterFree --disable asm_is_nop
+#include <stdlib.h>
+
+int main(void) {
+  int *x = malloc(16);
+  free(x);
+  // write
+  asm ("nop" : "=x" (*x)); // WARN
+  // read
+  asm ("nop" : : "x" (*x)); // WARN
+}

From a1caa655af30f2216ba45d17ab566569e71b8f6c Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 25 Jan 2024 10:04:02 +0100
Subject: [PATCH 47/62] our tests pass make test (random tests fail though for
 some reason)

---
 tests/regression/79-assembly/07-asm-exp-split.c   | 4 ++--
 tests/regression/79-assembly/100-invalidate-asm.c | 9 ---------
 tests/regression/79-assembly/32-asm-mem-leak.c    | 4 ++--
 3 files changed, 4 insertions(+), 13 deletions(-)
 delete mode 100644 tests/regression/79-assembly/100-invalidate-asm.c

diff --git a/tests/regression/79-assembly/07-asm-exp-split.c b/tests/regression/79-assembly/07-asm-exp-split.c
index 75ee44f693..c686ee337f 100644
--- a/tests/regression/79-assembly/07-asm-exp-split.c
+++ b/tests/regression/79-assembly/07-asm-exp-split.c
@@ -6,7 +6,7 @@ int main(void) {
   __goblint_split_begin(x);
   x = r ? 1 : 0;
   asm("nop" : "=x" (x), "=x" (r));
-  __goblint_check(x == 0 || x == 1);
+  __goblint_check(x == 0 || x == 1); // UNKNOWN (without asm it would be known)
   __goblint_split_end(x);
-  __goblint_check(x == 0 || x == 1); // UNKNOWN (intentionally)
+  __goblint_check(x == 0 || x == 1); // UNKNOWN
 }
diff --git a/tests/regression/79-assembly/100-invalidate-asm.c b/tests/regression/79-assembly/100-invalidate-asm.c
deleted file mode 100644
index 4e53a8163d..0000000000
--- a/tests/regression/79-assembly/100-invalidate-asm.c
+++ /dev/null
@@ -1,9 +0,0 @@
-//PARAM: --disable asm_is_nop
-#include <goblint.h>
-
-int main(void) {
-  int x = 0;
-  asm ("nop" : "=x" (x));
-  __goblint_check(x == 0); //WARN
-  return 0;
-}
diff --git a/tests/regression/79-assembly/32-asm-mem-leak.c b/tests/regression/79-assembly/32-asm-mem-leak.c
index 9572a7e842..0ffbeb3c57 100644
--- a/tests/regression/79-assembly/32-asm-mem-leak.c
+++ b/tests/regression/79-assembly/32-asm-mem-leak.c
@@ -12,8 +12,8 @@ void ok(void) {
 void not_ok(void) {
   char *x = malloc(64);
   asm ("nop" : "=x" (x));
-  free(x);
-  return; //WARN
+  free(x); //WARN
+  return;
 }
 
 int main(void) {

From 70307155cefb4297d95c916fef94ee6657495205 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 25 Jan 2024 10:28:21 +0100
Subject: [PATCH 48/62] mod-since-setjmp-test

---
 .../04-asm-modified-since-setjmp.c            | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 tests/regression/79-assembly/04-asm-modified-since-setjmp.c

diff --git a/tests/regression/79-assembly/04-asm-modified-since-setjmp.c b/tests/regression/79-assembly/04-asm-modified-since-setjmp.c
new file mode 100644
index 0000000000..dcc6dedab7
--- /dev/null
+++ b/tests/regression/79-assembly/04-asm-modified-since-setjmp.c
@@ -0,0 +1,20 @@
+#include <setjmp.h>
+
+jmp_buf buf;
+
+int main(void) {
+  int x;
+start:
+  x = 5;
+  if (setjmp(buf)) {
+    //read
+    asm ("nop" : : "x" (x));
+    return 0;
+  } else {
+    //write
+    asm goto ("nop" : "=x" (x) : : : exit2, exit); //WARN
+    longjmp(buf, 1);
+  }
+exit2:
+exit: return 0;
+}

From e2e2becad092e8819dad67db3f9e70a5ad49de07 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 25 Jan 2024 10:53:51 +0100
Subject: [PATCH 49/62] test

---
 src/analyses/base.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 4d48d2439f..f0ec31b28e 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1242,6 +1242,7 @@ struct
           if AD.mem Addr.UnknownPtr jmp_buf then
             M.warn ~category:Imprecise "Jump buffer %a may contain unknown pointers." d_exp e;
           begin match get ~ctx ~top:(VD.bot ()) ctx.local jmp_buf None with
+            (* dummy *)
             | JmpBuf (x, copied, invalid) ->
               if copied then
                 M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e;

From ae41a07224185fa939cc796724170ba480950dda Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Konrad=20G=C3=B6=C3=9Fmann?= <konrad.goessmann@tum.de>
Date: Thu, 25 Jan 2024 10:57:44 +0100
Subject: [PATCH 50/62] Removes merge annotation

---
 src/analyses/base.ml | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 4d48d2439f..a22b26b4b3 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2586,13 +2586,8 @@ struct
     | Setjmp { env }, _ ->
       let st' = match eval_rv ~ctx st env with
         | Address jmp_buf ->
-<<<<<<< HEAD
           let value = VD.JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, ctx.control_context ())), false, false) in
-          let r = set ~ctx ask gs st jmp_buf (Cilfacade.typeOf env) value in
-=======
-          let value = VD.JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, ctx.control_context ())), false) in
           let r = set ~ctx st jmp_buf (Cilfacade.typeOf env) value in
->>>>>>> 71e21b27973c78ef58c2567e314e128cfbb10564
           if M.tracing then M.tracel "setjmp" "setting setjmp %a on %a -> %a\n" d_exp env D.pretty st D.pretty r;
           r
         | _ -> failwith "problem?!"

From 2b62fcfcfd3409a5622141306e122c5bc6ff1e08 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Konrad=20G=C3=B6=C3=9Fmann?= <konrad.goessmann@tum.de>
Date: Thu, 25 Jan 2024 11:23:04 +0100
Subject: [PATCH 51/62] Fixes Build Error after changes to ctx

---
 src/analyses/base.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index a22b26b4b3..3f14807c6c 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2942,7 +2942,7 @@ struct
       end
     | Events.Invalidate {lvals} ->
       let exps = List.map Cil.mkAddrOrStartOf lvals in
-      invalidate ~ctx (Analyses.ask_of_ctx ctx) ctx.global st exps
+      invalidate ~ctx st exps
     | _ ->
       ctx.local
 end

From f0dcc9709ff3c8fc203e262abf061034bc0545ee Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 25 Jan 2024 11:51:49 +0100
Subject: [PATCH 52/62] var-eq-test

---
 src/analyses/base.ml                         |  3 +--
 tests/regression/79-assembly/05-asm-var-eq.c | 22 ++++++++++++++++++++
 2 files changed, 23 insertions(+), 2 deletions(-)
 create mode 100644 tests/regression/79-assembly/05-asm-var-eq.c

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index f06100bf97..3f14807c6c 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1242,7 +1242,6 @@ struct
           if AD.mem Addr.UnknownPtr jmp_buf then
             M.warn ~category:Imprecise "Jump buffer %a may contain unknown pointers." d_exp e;
           begin match get ~ctx ~top:(VD.bot ()) ctx.local jmp_buf None with
-            (* dummy *)
             | JmpBuf (x, copied, invalid) ->
               if copied then
                 M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e;
@@ -2943,7 +2942,7 @@ struct
       end
     | Events.Invalidate {lvals} ->
       let exps = List.map Cil.mkAddrOrStartOf lvals in
-      invalidate ~ctx (Analyses.ask_of_ctx ctx) ctx.global st exps
+      invalidate ~ctx st exps
     | _ ->
       ctx.local
 end
diff --git a/tests/regression/79-assembly/05-asm-var-eq.c b/tests/regression/79-assembly/05-asm-var-eq.c
new file mode 100644
index 0000000000..ff53cbcb54
--- /dev/null
+++ b/tests/regression/79-assembly/05-asm-var-eq.c
@@ -0,0 +1,22 @@
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --disable asm_is_nop
+#include<goblint.h>
+#include<stdio.h>
+
+void not_ok(int x) {
+  int y = x;
+  asm ("nop" : "=x" (x));
+  __goblint_check(x == y); // UNKNOWN
+}
+
+void ok(int x) {
+  asm ("nop" : "=x" (x));
+  int y = x;
+  __goblint_check(x == y);
+}
+
+int main() {
+  int x;
+  scanf("%d", &x);
+  ok(x);
+  not_ok(x);
+}

From 01cf846645ad1e98d9c187139f04d98090906d61 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 25 Jan 2024 11:58:43 +0100
Subject: [PATCH 53/62] uninit-test

---
 tests/regression/79-assembly/06-asm-uninit.c | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 tests/regression/79-assembly/06-asm-uninit.c

diff --git a/tests/regression/79-assembly/06-asm-uninit.c b/tests/regression/79-assembly/06-asm-uninit.c
new file mode 100644
index 0000000000..a02c6c4393
--- /dev/null
+++ b/tests/regression/79-assembly/06-asm-uninit.c
@@ -0,0 +1,8 @@
+// PARAM: --set ana.activated[+] uninit --disable asm_is_nop
+
+int main() {
+  int x, y, z;
+  asm ("nop" : "=x" (y) : "x" (x)); // WARN
+  z = y + 1; // NOWARN
+  return 0;
+}

From 2741b3277f4b0f13c8bae59f6e1239be03716759 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 25 Jan 2024 14:29:23 +0100
Subject: [PATCH 54/62] ups

---
 src/analyses/malloc_null.ml | 24 +++++++++++-------------
 src/analyses/mayLocks.ml    |  1 -
 src/maingoblint.ml          |  3 ---
 3 files changed, 11 insertions(+), 17 deletions(-)

diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 588cefc529..3b98d25d76 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -17,9 +17,19 @@ struct
   module C = ValueDomain.AddrSetDomain
   module P = IdentityP (D)
 
+  let name () = "malloc_null"
+
+  let return_addr_ = ref Addr.NullPtr
+  let return_addr () = !return_addr_
+
+  let startstate v = D.empty ()
+  let threadenter ctx ~multiple lval f args = [D.empty ()]
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
+  let exitstate  v = D.empty ()
   let ignore_asm = ref true
 
-  let init _ =
+  let init marshal =
+    return_addr_ :=  Addr.of_var (Cilfacade.create_var @@ makeVarinfo false "RETURN" voidType);
     ignore_asm := get_bool "asm_is_nop"
 
   (*
@@ -176,9 +186,6 @@ struct
   let body ctx (f:fundec) : D.t =
     ctx.local
 
-  let return_addr_ = ref Addr.NullPtr
-  let return_addr () = !return_addr_
-
   let return ctx (exp:exp option) (f:fundec) : D.t =
     let remove_var x v = List.fold_right D.remove (to_addrs v) x in
     let nst = List.fold_left remove_var ctx.local (f.slocals @ f.sformals) in
@@ -228,15 +235,6 @@ struct
       end
     | _ -> ctx.local
 
-  let name () = "malloc_null"
-
-  let startstate v = D.empty ()
-  let threadenter ctx ~multiple lval f args = [D.empty ()]
-  let threadspawn ctx ~multiple lval f args fctx = ctx.local
-  let exitstate  v = D.empty ()
-
-  let init marshal =
-    return_addr_ :=  Addr.of_var (Cilfacade.create_var @@ makeVarinfo false "RETURN" voidType)
 end
 
 let _ =
diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml
index 0a0e39e898..bd1240a8e7 100644
--- a/src/analyses/mayLocks.ml
+++ b/src/analyses/mayLocks.ml
@@ -36,7 +36,6 @@ struct
       (let mtype = ctx.ask (Queries.MutexType (v, Offset.Unit.of_offs o)) in
        match mtype with
        | `Lifted MutexAttrDomain.MutexKind.NonRec -> D.remove l ctx.local
-       (* todo [IMPORTANT]: find out why the else branch is always taken at invalidate *)
        | _ -> ctx.local (* we cannot remove them here *))
     | None -> ctx.local (* we cannot remove them here *)
 
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index cc7bfc26c1..f1d2793d2e 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -415,11 +415,8 @@ let preprocess_files () =
 
   let preprocessed =
     List.concat_map preprocess_arg_file (List.map Fpath.v (get_string_list "files"))
-    (* todo: uncomment; for testing only *)
-    (*
     @
     List.concat_map (preprocess_arg_file ~preprocess:true) !extra_files
-    *)
   in
   if not (get_bool "pre.exist") then (
     let preprocess_tasks = List.filter_map snd preprocessed in

From efdb7ffcae7c4174dae36689ac746c606d3262f7 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 25 Jan 2024 14:43:51 +0100
Subject: [PATCH 55/62] big ups

---
 src/analyses/useAfterFree.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index f20572512c..70a3c1733e 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -175,6 +175,10 @@ struct
     warn_exp_might_contain_freed "assign" ctx rval;
     ctx.local
 
+  let branch ctx (exp:exp) (tv:bool) : D.t =
+    warn_exp_might_contain_freed "branch" ctx exp;
+    ctx.local
+
   let asm ctx =
     if not !ignore_asm then begin
       let ins, outs = Analyses.asm_extract_ins_outs ctx in

From cd1c3652eea77634c0bcc67bd90ba0de289787eb Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Thu, 1 Feb 2024 11:43:21 +0100
Subject: [PATCH 56/62] bugfixes; mutex-test

---
 src/analyses/deadlock.ml                    |  4 ----
 src/analyses/locksetAnalysis.ml             |  2 +-
 src/analyses/mayLocks.ml                    |  2 --
 src/common/framework/cfgTools.ml            | 15 ++++++++-------
 tests/practical/mem-leak.c                  |  2 +-
 tests/regression/79-assembly/08-asm-mutex.c | 14 ++++++++++++++
 6 files changed, 24 insertions(+), 15 deletions(-)
 create mode 100644 tests/regression/79-assembly/08-asm-mutex.c

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 57078158ab..38aafef7a3 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -40,10 +40,6 @@ struct
     let remove ctx l =
       let inLockAddrs (e, _, _) = Lock.equal l e in
       D.filter (neg inLockAddrs) ctx.local
-
-    let is_held ctx l =
-      let inLockAddrs (e, _, _) = Lock.equal l e in
-      D.exists inLockAddrs ctx.local
       
   end
 
diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml
index 3fa9a3043f..3582d147e1 100644
--- a/src/analyses/locksetAnalysis.ml
+++ b/src/analyses/locksetAnalysis.ml
@@ -32,7 +32,6 @@ sig
 
   val add: (D.t, G.t, D.t, V.t) ctx -> LockDomain.Lockset.Lock.t -> D.t
   val remove: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> D.t
-  val is_held: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> bool
 end
 
 let addr_set_of_lval (a: Queries.ask) lval =
@@ -76,6 +75,7 @@ module type MustArg =
 sig
   include MayArg
   val remove_all: (D.t, _, D.t, _) ctx -> D.t
+  val is_held: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> bool
 end
 
 module MakeMust (Arg: MustArg) =
diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml
index bd1240a8e7..853005de87 100644
--- a/src/analyses/mayLocks.ml
+++ b/src/analyses/mayLocks.ml
@@ -38,8 +38,6 @@ struct
        | `Lifted MutexAttrDomain.MutexKind.NonRec -> D.remove l ctx.local
        | _ -> ctx.local (* we cannot remove them here *))
     | None -> ctx.local (* we cannot remove them here *)
-
-  let is_held ctx l = D.mem l ctx.local
 end
 
 module Spec =
diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml
index 40c040e3ab..2edcc5a925 100644
--- a/src/common/framework/cfgTools.ml
+++ b/src/common/framework/cfgTools.ml
@@ -378,17 +378,18 @@ let createCFG (file: file) =
             begin match real_succs () with
               | [] -> failwith "MyCFG.createCFG: 0 Asm succ"
               | [succ, skippedStatements] -> begin
-                addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, false)) (Statement succ);
-                if not (get_bool "asm_is_nop") then
+                if get_bool "asm_is_nop" then begin
+                  addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, false)) (Statement succ);
+                end 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
+                    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
+                    | None -> (succ', skippedStatements') :: acc
+                    ) [(succ, skippedStatements)] labels in
                   List.iter (fun (succ, skippedStatements) ->
                     addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, true)) (Statement succ)
-                  ) unique_dests;
+                    ) unique_dests;
               end
               | _ -> failwith "MyCFG.createCFG: >1 Asm succ"
             end
diff --git a/tests/practical/mem-leak.c b/tests/practical/mem-leak.c
index f67b9f53e6..b54abdb56d 100644
--- a/tests/practical/mem-leak.c
+++ b/tests/practical/mem-leak.c
@@ -3,7 +3,7 @@
 int main(void) {
   char *x = malloc(64);
   char *y = x;
-  asm ("nop" : "=x" (*x));
   free(y);
+exit:
   return 0;
 }
diff --git a/tests/regression/79-assembly/08-asm-mutex.c b/tests/regression/79-assembly/08-asm-mutex.c
new file mode 100644
index 0000000000..eefacbbb6f
--- /dev/null
+++ b/tests/regression/79-assembly/08-asm-mutex.c
@@ -0,0 +1,14 @@
+// PARAM: --set ana.activated[+] mutexEvents --disable asm_is_nop
+#include <pthread.h>
+
+pthread_mutex_t mutex;
+
+int main() {
+    int x = 2;
+    pthread_mutex_init(&mutex, NULL);
+    pthread_mutex_lock(&mutex);
+    asm ("nop" : "=g" (mutex), "=x" (x));
+    pthread_mutex_unlock(&mutex); // WARN
+    return 0;
+}
+

From cdb6a3e185ba37f4e6c03ddada7c129ea275dcbe Mon Sep 17 00:00:00 2001
From: ge46lup <ge46lup@tum.de>
Date: Fri, 2 Feb 2024 01:25:46 +0100
Subject: [PATCH 57/62] asm tests

---
 tests/regression/65-taint/02-invalidate.c  |  2 +-
 tests/regression/79-assembly/55-asm-taint  | 27 ++++++++++++++++++++++
 tests/regression/79-assembly/58-asm-region | 13 +++++++++++
 3 files changed, 41 insertions(+), 1 deletion(-)
 create mode 100644 tests/regression/79-assembly/55-asm-taint
 create mode 100644 tests/regression/79-assembly/58-asm-region

diff --git a/tests/regression/65-taint/02-invalidate.c b/tests/regression/65-taint/02-invalidate.c
index cf4636192f..1b0010118e 100644
--- a/tests/regression/65-taint/02-invalidate.c
+++ b/tests/regression/65-taint/02-invalidate.c
@@ -4,7 +4,7 @@
 extern void unknown_fun (int *a);
 
 void mainfunct(int *rptr, int* uptr) {
-  unknown_fun(rptr);
+      unknown_fun(rptr);
 }
 
 int g;
diff --git a/tests/regression/79-assembly/55-asm-taint b/tests/regression/79-assembly/55-asm-taint
new file mode 100644
index 0000000000..0a8b40e718
--- /dev/null
+++ b/tests/regression/79-assembly/55-asm-taint
@@ -0,0 +1,27 @@
+//PARAM --set "ana.activated[+]" taintPartialContexts --set ana.ctx_insens[+] base
+#include <goblint.h>
+
+
+void mainfunct(int *rptr, int* uptr) {
+      asm("nop" : "=x"(*rptr));
+}
+
+int g;
+
+int main() {
+  int r, u;
+
+  g = 1;
+  r = 1;
+  u = 1;
+  mainfunct(&r, &u);
+
+  g = 2;
+  r = 2;
+  u = 2;
+  mainfunct(&r, &u);
+
+  __goblint_check(g == 2); //UNKNOWN!
+  __goblint_check(r == 2); //UNKNOWN!
+  __goblint_check(u == 2);
+}
diff --git a/tests/regression/79-assembly/58-asm-region b/tests/regression/79-assembly/58-asm-region
new file mode 100644
index 0000000000..64ffe469bb
--- /dev/null
+++ b/tests/regression/79-assembly/58-asm-region
@@ -0,0 +1,13 @@
+//PARAM: --set ana.activated[+] region --disable asm_is_nop
+#include <stdlib.h>
+
+int main() {
+    char *buffer = malloc(256);  
+    buffer[0] = 'a';            
+
+    
+    __asm__("movb $0, %0" : "=m" (*buffer));
+
+    free(buffer);               
+    return 0;
+}

From 83b5a7cbc037140de2815972b3a477d0a91298ae Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Mon, 5 Feb 2024 16:53:15 +0100
Subject: [PATCH 58/62] adding outs ins params makes goblint segfault every
 time (compiles)

---
 goblint.opam                              |  2 +-
 src/analyses/accessAnalysis.ml            |  3 +-
 src/analyses/base.ml                      |  6 +--
 src/analyses/expsplit.ml                  |  5 +-
 src/analyses/mCP.ml                       |  2 +-
 src/analyses/malloc_null.ml               |  3 +-
 src/analyses/unassumeAnalysis.ml          |  2 +-
 src/analyses/uninit.ml                    |  3 +-
 src/analyses/useAfterFree.ml              |  3 +-
 src/cdomain/value/cdomains/valueDomain.ml |  2 +-
 src/framework/analyses.ml                 |  7 +--
 src/framework/constraints.ml              | 61 ++++++++++++-----------
 src/util/wideningTokens.ml                | 14 +++---
 src/witness/witnessConstraints.ml         |  2 +-
 14 files changed, 57 insertions(+), 58 deletions(-)

diff --git a/goblint.opam b/goblint.opam
index 871ac17739..7a75a1fb45 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -77,7 +77,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/N0W0RK/goblint-cil.git#second_try" ]
+  # [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#d2760bacfbfdb25a374254de44f2ff1cb5f42abd" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
 ]
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index 327feb8d62..4e46f96b2a 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -75,9 +75,8 @@ struct
       ctx.local
     end
 
-  let asm ctx =
+  let asm ctx outs ins =
     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;
       (* deref needs to be set to true because we have to use AddrOf *)
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 3f14807c6c..ddaa88e04f 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2902,11 +2902,9 @@ struct
     in
     D.join ctx.local e_d'
 
-  let asm ctx = 
-    if not !ignore_asm then begin
-      let _, outs = Analyses.asm_extract_ins_outs ctx in
+  let asm ctx outs ins = 
+    if not !ignore_asm then
       ctx.emit (Events.Invalidate {lvals=outs});
-    end;
     ctx.local
 
   let event ctx e octx =
diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml
index fa5be0e289..5758068eba 100644
--- a/src/analyses/expsplit.ml
+++ b/src/analyses/expsplit.ml
@@ -99,9 +99,10 @@ struct
     | Invalidate {lvals} ->
       let handle_lval local lval =
         let exp = Lval lval in
-        if D.mem exp local then begin
+        if D.mem exp local then
           D.remove exp local
-        end else local
+        else
+          local
       in
       List.fold handle_lval ctx.local lvals
     | _ ->
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 50f6d5409b..bb5cea9ced 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -428,7 +428,7 @@ struct
     if q then raise Deadcode else d
 
 
-  let asm (ctx:(D.t, G.t, C.t, V.t) ctx) =
+  let asm (ctx:(D.t, G.t, C.t, V.t) ctx) outs ins =
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 3b98d25d76..0946b9f544 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -169,9 +169,8 @@ struct
       D.add (Addr.of_mval mval) ctx.local
     | _ -> ctx.local
 
-  let asm ctx =
+  let asm ctx outs ins =
     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;
       let handle_out lval = warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local (Lval lval) in
diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index 5895f242c9..3939efa517 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -304,7 +304,7 @@ struct
 
     emit_unassume {ctx with local = st} (* doesn't query, so no need to redefine ask *)
 
-  let asm ctx =
+  let asm ctx outs ins =
     emit_unassume ctx
 
   let skip ctx =
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index 84536e6bf8..20043ad50d 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -229,9 +229,8 @@ struct
     ignore (is_expr_initd (Analyses.ask_of_ctx ctx) rval ctx.local);
     init_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
-  let asm ctx = 
+  let asm ctx outs ins = 
     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
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index 70a3c1733e..b29741bd21 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -179,9 +179,8 @@ struct
     warn_exp_might_contain_freed "branch" ctx exp;
     ctx.local
 
-  let asm ctx =
+  let asm ctx outs ins =
     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;
       let handle_in exp = warn_exp_might_contain_freed "asm" ctx exp in
diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml
index 80614c52dd..3f42978167 100644
--- a/src/cdomain/value/cdomains/valueDomain.ml
+++ b/src/cdomain/value/cdomains/valueDomain.ml
@@ -724,7 +724,7 @@ struct
       Array (CArrays.set ask n (array_idx_top) v)
     |                 t , Blob n       -> Blob (Blobs.invalidate_value ask t n)
     |                 _ , Thread tid   -> Thread (Threads.join (Threads.top ()) tid)
-    |                 _ , JmpBuf (b, c, _)     -> JmpBuf(b, c, true)
+    |                 _ , JmpBuf (b, c, _)     -> JmpBuf(b, c, true) (* TODO: no top jmpbuf *)
     | _, Bot -> Bot (* Leave uninitialized value (from malloc) alone in free to avoid trashing everything. TODO: sound? *)
     |                 t , _             -> top_value t
 
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 53f45242aa..29e02617fc 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -238,8 +238,9 @@ sig
       "return exp" or "return" in the passed function (fundec) *)
   val return: (D.t, G.t, C.t, V.t) ctx -> exp option  -> fundec -> D.t
 
-  (** A transfer function meant to handle inline assembler program points *)
-  val asm   : (D.t, G.t, C.t, V.t) ctx -> D.t
+  (** A transfer function meant to handle inline assembler program points.
+      It gets outputs (written by asm) and inputs (read by asm) as arguments. *)
+  val asm   : (D.t, G.t, C.t, V.t) ctx -> lval list -> exp list -> D.t
 
   (** A transfer function which works as the identity function, i.e., it skips and does nothing.
       Used for empty loops. *)
@@ -364,7 +365,7 @@ struct
 
   let vdecl ctx _ = ctx.local
 
-  let asm ctx =
+  let asm ctx outs ins =
     if get_bool "asm_is_nop" then begin
       M.msg_final Info ~category:Unsound "ASM ignored";
       M.info ~category:Unsound "ASM statement ignored.";
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 4a093494e5..7281be2650 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -71,8 +71,8 @@ struct
   let return ctx r f =
     D.lift @@ S.return (conv ctx) r f
 
-  let asm ctx =
-    D.lift @@ S.asm (conv ctx)
+  let asm ctx outs ins =
+    D.lift @@ S.asm (conv ctx) outs ins
 
   let skip ctx =
     D.lift @@ S.skip (conv ctx)
@@ -244,13 +244,13 @@ struct
   let sync ctx reason = lift_fun ctx (lift ctx) S.sync   ((|>) reason)
   let query' ctx (type a) (q: a Queries.t): a Queries.result =
     lift_fun ctx identity   S.query  (fun x -> x q)
-  let assign ctx lv e = lift_fun ctx (lift ctx) S.assign ((|>) e % (|>) lv)
-  let vdecl ctx v     = lift_fun ctx (lift ctx) S.vdecl  ((|>) v)
-  let branch ctx e tv = lift_fun ctx (lift ctx) S.branch ((|>) tv % (|>) e)
-  let body ctx f      = lift_fun ctx (lift ctx) S.body   ((|>) f)
-  let return ctx r f  = lift_fun ctx (lift ctx) S.return ((|>) f % (|>) r)
-  let asm ctx         = lift_fun ctx (lift ctx) S.asm    identity
-  let skip ctx        = lift_fun ctx (lift ctx) S.skip   identity
+  let assign ctx lv e  = lift_fun ctx (lift ctx) S.assign ((|>) e % (|>) lv)
+  let vdecl ctx v      = lift_fun ctx (lift ctx) S.vdecl  ((|>) v)
+  let branch ctx e tv  = lift_fun ctx (lift ctx) S.branch ((|>) tv % (|>) e)
+  let body ctx f       = lift_fun ctx (lift ctx) S.body   ((|>) f)
+  let return ctx r f   = lift_fun ctx (lift ctx) S.return ((|>) f % (|>) r)
+  let asm ctx outs ins = lift_fun ctx (lift ctx) S.asm    ((|>) ins % (|>) outs)
+  let skip ctx         = lift_fun ctx (lift ctx) S.skip   identity
   let special ctx r f args        = lift_fun ctx (lift ctx) S.special ((|>) args % (|>) f % (|>) r)
   let combine_env' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_env (fun p -> p r fe f args fc (fst es) f_ask)
   let combine_assign' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
@@ -387,15 +387,15 @@ struct
     }
   let lift_fun ctx f g = g (f (conv ctx)), snd ctx.local
 
-  let sync ctx reason = lift_fun ctx S.sync   ((|>) reason)
-  let query ctx       = S.query (conv ctx)
-  let assign ctx lv e = lift_fun ctx S.assign ((|>) e % (|>) lv)
-  let vdecl ctx v     = lift_fun ctx S.vdecl  ((|>) v)
-  let branch ctx e tv = lift_fun ctx S.branch ((|>) tv % (|>) e)
-  let body ctx f      = lift_fun ctx S.body   ((|>) f)
-  let return ctx r f  = lift_fun ctx S.return ((|>) f % (|>) r)
-  let asm ctx         = lift_fun ctx S.asm    identity
-  let skip ctx        = lift_fun ctx S.skip   identity
+  let sync ctx reason  = lift_fun ctx S.sync   ((|>) reason)
+  let query ctx        = S.query (conv ctx)
+  let assign ctx lv e  = lift_fun ctx S.assign ((|>) e % (|>) lv)
+  let vdecl ctx v      = lift_fun ctx S.vdecl  ((|>) v)
+  let branch ctx e tv  = lift_fun ctx S.branch ((|>) tv % (|>) e)
+  let body ctx f       = lift_fun ctx S.body   ((|>) f)
+  let return ctx r f   = lift_fun ctx S.return ((|>) f % (|>) r)
+  let asm ctx outs ins = lift_fun ctx S.asm    ((|>) ins % (|>) outs)
+  let skip ctx         = lift_fun ctx S.skip   identity
   let special ctx r f args       = lift_fun ctx S.special ((|>) args % (|>) f % (|>) r)
 
   let event ctx e octx = lift_fun ctx S.event ((|>) (conv octx) % (|>) e)
@@ -480,13 +480,13 @@ struct
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     lift_fun ctx identity S.query (fun (x) -> x q) (Queries.Result.bot q)
-  let assign ctx lv e = lift_fun ctx D.lift   S.assign ((|>) e % (|>) lv) `Bot
-  let vdecl ctx v     = lift_fun ctx D.lift   S.vdecl  ((|>) v)            `Bot
-  let branch ctx e tv = lift_fun ctx D.lift   S.branch ((|>) tv % (|>) e) `Bot
-  let body ctx f      = lift_fun ctx D.lift   S.body   ((|>) f)            `Bot
-  let return ctx r f  = lift_fun ctx D.lift   S.return ((|>) f % (|>) r)  `Bot
-  let asm ctx         = lift_fun ctx D.lift   S.asm    identity           `Bot
-  let skip ctx        = lift_fun ctx D.lift   S.skip   identity           `Bot
+  let assign ctx lv e  = lift_fun ctx D.lift   S.assign ((|>) e % (|>) lv) `Bot
+  let vdecl ctx v      = lift_fun ctx D.lift   S.vdecl  ((|>) v)            `Bot
+  let branch ctx e tv  = lift_fun ctx D.lift   S.branch ((|>) tv % (|>) e) `Bot
+  let body ctx f       = lift_fun ctx D.lift   S.body   ((|>) f)            `Bot
+  let return ctx r f   = lift_fun ctx D.lift   S.return ((|>) f % (|>) r)  `Bot
+  let asm ctx outs ins = lift_fun ctx D.lift   S.asm    ((|>) ins % (|>) outs)  `Bot
+  let skip ctx         = lift_fun ctx D.lift   S.skip   identity           `Bot
   let special ctx r f args       = lift_fun ctx D.lift S.special ((|>) args % (|>) f % (|>) r)        `Bot
   let combine_env ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_env (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
@@ -765,9 +765,12 @@ struct
     end else
       common_joins ctx funs !r !spawns
 
-  let tf_asm var edge prev_node getl sidel getg sideg d =
+  let tf_asm var edge prev_node outs ins getl sidel getg sideg d =
+    let third (_, _, x) = x in
+    let outs = Util.list_map third outs in
+    let ins = Util.list_map third ins in
     let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
-    common_join ctx (S.asm ctx) !r !spawns
+    common_join ctx (S.asm ctx outs ins) !r !spawns
 
   let tf_skip var edge prev_node getl sidel getg sideg d =
     let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
@@ -781,7 +784,7 @@ struct
       | Entry f         -> tf_entry var edge prev_node f
       | Ret (r,fd)      -> tf_ret var edge prev_node r fd
       | Test (p,b)      -> tf_test var edge prev_node p b
-      | ASM (_, _, _,_) -> tf_asm var edge prev_node (* TODO: use ASM fields for something? *)
+      | ASM (_, outs, ins,_) -> tf_asm var edge prev_node outs ins
       | Skip            -> tf_skip var edge prev_node
     end getl sidel getg sideg d
 
@@ -1098,7 +1101,7 @@ struct
   let body   ctx f      = map ctx Spec.body    (fun h -> h f   )
   let return ctx e f    = map ctx Spec.return  (fun h -> h e f )
   let branch ctx e tv   = map ctx Spec.branch  (fun h -> h e tv)
-  let asm ctx           = map ctx Spec.asm     identity
+  let asm ctx outs ins  = map ctx Spec.asm     (fun h -> h outs ins)
   let skip ctx          = map ctx Spec.skip    identity
   let special ctx l f a = map ctx Spec.special (fun h -> h l f a)
 
diff --git a/src/util/wideningTokens.ml b/src/util/wideningTokens.ml
index 1816de90c7..d71ade1851 100644
--- a/src/util/wideningTokens.ml
+++ b/src/util/wideningTokens.ml
@@ -168,13 +168,13 @@ struct
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     lift_fun ctx Fun.const S.query (fun (x) -> x q)
-  let assign ctx lv e = lift_fun ctx lift'   S.assign ((|>) e % (|>) lv)
-  let vdecl ctx v     = lift_fun ctx lift'   S.vdecl  ((|>) v)
-  let branch ctx e tv = lift_fun ctx lift'   S.branch ((|>) tv % (|>) e)
-  let body ctx f      = lift_fun ctx lift'   S.body   ((|>) f)
-  let return ctx r f  = lift_fun ctx lift'   S.return ((|>) f % (|>) r)
-  let asm ctx         = lift_fun ctx lift'   S.asm    identity
-  let skip ctx        = lift_fun ctx lift'   S.skip   identity
+  let assign ctx lv e  = lift_fun ctx lift'   S.assign ((|>) e % (|>) lv)
+  let vdecl ctx v      = lift_fun ctx lift'   S.vdecl  ((|>) v)
+  let branch ctx e tv  = lift_fun ctx lift'   S.branch ((|>) tv % (|>) e)
+  let body ctx f       = lift_fun ctx lift'   S.body   ((|>) f)
+  let return ctx r f   = lift_fun ctx lift'   S.return ((|>) f % (|>) r)
+  let asm ctx outs ins = lift_fun ctx lift'   S.asm    ((|>) ins % (|>) outs)
+  let skip ctx         = lift_fun ctx lift'   S.skip   identity
   let special ctx r f args       = lift_fun ctx lift' S.special ((|>) args % (|>) f % (|>) r)
   let combine_env ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_env (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
   let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index 8dedf77a79..188819a7ef 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -189,7 +189,7 @@ struct
   let body   ctx f      = map ctx Spec.body    (fun h -> h f   )
   let return ctx e f    = map ctx Spec.return  (fun h -> h e f )
   let branch ctx e tv   = map ctx Spec.branch  (fun h -> h e tv)
-  let asm ctx           = map ctx Spec.asm     identity
+  let asm ctx outs ins  = map ctx Spec.asm     (fun h -> h outs ins)
   let skip ctx          = map ctx Spec.skip    identity
   let special ctx l f a = map ctx Spec.special (fun h -> h l f a)
   let event ctx e octx = map_event ctx e (* TODO: ???? *)

From 8abe7a6da2b80ffbba9123d62435de1068f04841 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Tue, 6 Feb 2024 07:26:47 +0100
Subject: [PATCH 59/62] wtf

---
 src/framework/analyses.ml    |  8 --------
 src/framework/constraints.ml | 10 +++++-----
 2 files changed, 5 insertions(+), 13 deletions(-)

diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 29e02617fc..44863ae062 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -177,14 +177,6 @@ let ctx_failwith s = raise (Ctx_failure s) (* TODO: use everywhere in ctx *)
 (** Convert [ctx] to [Queries.ask]. *)
 let ask_of_ctx ctx: Queries.ask = { Queries.f = ctx.ask }
 
-let asm_extract_ins_outs ctx = 
-  match ctx.edge with
-  | ASM (_, asm_out, asm_in, _) ->
-    let third (_, _, x) = x in
-    List.map third asm_in,
-    List.map third asm_out
-  | _ -> failwith "can't call asm_extract_ins_outs outside of transfer function asm"
-
 module type Spec =
 sig
   module D : Lattice.S
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 7281be2650..0b379221fc 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -155,8 +155,8 @@ struct
   let return ctx r f =
     S.return (conv ctx) r f
 
-  let asm ctx =
-    S.asm (conv ctx)
+  let asm ctx outs ins =
+    S.asm (conv ctx) outs ins
 
   let skip ctx =
     S.skip (conv ctx)
@@ -1301,7 +1301,7 @@ struct
   let threadspawn ctx ~multiple lv f args fctx = S.threadspawn (conv ctx) ~multiple lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
-  let asm ctx = S.asm (conv ctx)
+  let asm ctx outs ins = S.asm (conv ctx) outs ins
   let event ctx e octx = S.event (conv ctx) e (conv octx)
 end
 
@@ -1543,7 +1543,7 @@ struct
   let threadspawn ctx ~multiple lv f args fctx = S.threadspawn (conv ctx) ~multiple lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
-  let asm ctx = S.asm (conv ctx)
+  let asm ctx outs ins = S.asm (conv ctx) outs ins
   let event ctx e octx = S.event (conv ctx) e (conv octx)
 end
 
@@ -1686,7 +1686,7 @@ struct
   let threadspawn ctx ~multiple lv f args fctx = S.threadspawn (conv ctx) ~multiple lv f args (conv fctx)
   let sync ctx = S.sync (conv ctx)
   let skip ctx = S.skip (conv ctx)
-  let asm ctx = S.asm (conv ctx)
+  let asm ctx outs ins = S.asm (conv ctx) outs ins
   let event ctx e octx = S.event (conv ctx) e (conv octx)
 end
 

From 7edfff066099e9b96ceee39ea3250a62707727b1 Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Tue, 6 Feb 2024 08:53:45 +0100
Subject: [PATCH 60/62] found bug :) why did ocaml no give a warning?

---
 src/analyses/mCP.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index bb5cea9ced..f17ef5e7b4 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -436,7 +436,7 @@ struct
     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 ~post_all ctx'' n d in
-      n, repr @@ S.asm ctx'
+      n, repr @@ S.asm ctx' outs ins
     in
     let d, q = map_deadcode f @@ spec_list ctx.local in
     do_sideg ctx !sides;

From a7b830d552c25e6dcc27c577e5c9e44dc1455f3d Mon Sep 17 00:00:00 2001
From: Simon Tietz <gandalf@toshi>
Date: Wed, 7 Feb 2024 17:50:03 +0100
Subject: [PATCH 61/62] bugfix

---
 src/common/framework/cfgTools.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml
index 2edcc5a925..dcc4cfa1e5 100644
--- a/src/common/framework/cfgTools.ml
+++ b/src/common/framework/cfgTools.ml
@@ -378,15 +378,14 @@ let createCFG (file: file) =
             begin match real_succs () with
               | [] -> failwith "MyCFG.createCFG: 0 Asm succ"
               | [succ, skippedStatements] -> begin
-                if get_bool "asm_is_nop" then begin
-                  addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, false)) (Statement succ);
-                end else
+                addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, false)) (Statement succ);
+                if not (get_bool "asm_is_nop") then
                   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
-                    ) [(succ, skippedStatements)] labels in
+                    | None when succ' != succ -> (succ', skippedStatements') :: acc
+                    | _ -> acc
+                    ) [] labels in
                   List.iter (fun (succ, skippedStatements) ->
                     addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, true)) (Statement succ)
                     ) unique_dests;

From 626b8e148bb006151c76013bc1df58624d6cb4fa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Konrad=20G=C3=B6=C3=9Fmann?= <konrad.goessmann@tum.de>
Date: Fri, 9 Feb 2024 22:37:59 +0100
Subject: [PATCH 62/62] Refactores regression tests.

---
 tests/practical/deadlock.c                    | 29 -------------------
 tests/practical/file-use.c                    |  9 ------
 tests/practical/mem-leak.c                    |  9 ------
 tests/practical/tmp-special.c                 |  7 -----
 tests/practical/uninit.c                      |  6 ----
 tests/practical/var-eq.c                      |  6 ----
 .../79-assembly/09-asm-invalidate-condvar.c   | 28 ++++++++++++++++++
 .../{28-asm_deadlock.c => 10-asm-deadlock.c}  |  0
 .../{32-asm-mem-leak.c => 11-asm-mem-leak.c}  |  0
 .../{55-asm-taint => 12-asm-taint.c}          |  2 +-
 ...7-jmpbuf-invalid.c => 13-jmpbuf-invalid.c} |  0
 .../{58-asm-region => 14-asm-region.c}        |  0
 .../79-assembly/15-jumpbuf-poison.c           | 25 ++++++++++++++++
 .../79-assembly/16-jumpbuf-read-poison.c      | 25 ++++++++++++++++
 14 files changed, 79 insertions(+), 67 deletions(-)
 delete mode 100644 tests/practical/deadlock.c
 delete mode 100644 tests/practical/file-use.c
 delete mode 100644 tests/practical/mem-leak.c
 delete mode 100644 tests/practical/tmp-special.c
 delete mode 100644 tests/practical/uninit.c
 delete mode 100644 tests/practical/var-eq.c
 create mode 100644 tests/regression/79-assembly/09-asm-invalidate-condvar.c
 rename tests/regression/79-assembly/{28-asm_deadlock.c => 10-asm-deadlock.c} (100%)
 rename tests/regression/79-assembly/{32-asm-mem-leak.c => 11-asm-mem-leak.c} (100%)
 rename tests/regression/79-assembly/{55-asm-taint => 12-asm-taint.c} (90%)
 rename tests/regression/79-assembly/{57-jmpbuf-invalid.c => 13-jmpbuf-invalid.c} (100%)
 rename tests/regression/79-assembly/{58-asm-region => 14-asm-region.c} (100%)
 create mode 100644 tests/regression/79-assembly/15-jumpbuf-poison.c
 create mode 100644 tests/regression/79-assembly/16-jumpbuf-read-poison.c

diff --git a/tests/practical/deadlock.c b/tests/practical/deadlock.c
deleted file mode 100644
index 5223caa0ed..0000000000
--- a/tests/practical/deadlock.c
+++ /dev/null
@@ -1,29 +0,0 @@
-#include <unistd.h>
-#include <pthread.h>
-#include <stdio.h>
-
-pthread_mutex_t lock_a;
-pthread_mutex_t lock_b;
-
-void *proc_a(void *arg) {
-    pthread_mutex_lock(&lock_a);
-    sleep(1);
-    pthread_mutex_lock(&lock_b);
-    pthread_exit(NULL);
-}
-
-void *proc_b(void *arg) {
-    pthread_mutex_lock(&lock_b);
-    sleep(1);
-    pthread_mutex_lock(&lock_a);
-    return NULL;
-}
-
-int main(void) {
-    pthread_t a, b;
-    pthread_create(&a, NULL, proc_a, NULL);
-    proc_b(NULL);
-    int x, y;
-    asm ("nop" : "=g" (lock_a), "=x" (x));
-    puts("no deadlock!");
-}
diff --git a/tests/practical/file-use.c b/tests/practical/file-use.c
deleted file mode 100644
index 0e5693172b..0000000000
--- a/tests/practical/file-use.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <stdio.h>
-
-int main(void) {
-  FILE *f = fopen("file-use.c", "r");
-  //int x;
-  //asm ("nop" : "=g" (f), "=g" (x));
-  fclose(f);
-  return 0;
-}
diff --git a/tests/practical/mem-leak.c b/tests/practical/mem-leak.c
deleted file mode 100644
index b54abdb56d..0000000000
--- a/tests/practical/mem-leak.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <stdlib.h>
-
-int main(void) {
-  char *x = malloc(64);
-  char *y = x;
-  free(y);
-exit:
-  return 0;
-}
diff --git a/tests/practical/tmp-special.c b/tests/practical/tmp-special.c
deleted file mode 100644
index 0195ef6d5c..0000000000
--- a/tests/practical/tmp-special.c
+++ /dev/null
@@ -1,7 +0,0 @@
-#include <math.h>
-
-int main(void) {
-  int x = floor(0.8);
-  asm ("nop" : "=x" (x));
-  return x;
-}
diff --git a/tests/practical/uninit.c b/tests/practical/uninit.c
deleted file mode 100644
index ad379f1634..0000000000
--- a/tests/practical/uninit.c
+++ /dev/null
@@ -1,6 +0,0 @@
-int main(void) {
-  int x;
-  int y;
-  asm ("nop" : "=x" (y) : "x" (x));
-  return y;
-}
diff --git a/tests/practical/var-eq.c b/tests/practical/var-eq.c
deleted file mode 100644
index 2f8d529984..0000000000
--- a/tests/practical/var-eq.c
+++ /dev/null
@@ -1,6 +0,0 @@
-int main(void) {
-    int x = 0;
-    int y = x;
-    asm ("mov $1, %0" : "=x" (x));
-    return 0;
-}
diff --git a/tests/regression/79-assembly/09-asm-invalidate-condvar.c b/tests/regression/79-assembly/09-asm-invalidate-condvar.c
new file mode 100644
index 0000000000..e6da610251
--- /dev/null
+++ b/tests/regression/79-assembly/09-asm-invalidate-condvar.c
@@ -0,0 +1,28 @@
+// PARAM: --set ana.activated[+] condvars --set ana.activated[+] taintPartialContexts --disable asm_is_nop
+#include <goblint.h>
+
+int glob;
+
+void f() {
+}
+
+int main() {
+  int unk;
+  int tv;
+  if (unk)
+    glob = 0;
+  else
+    glob = 10;
+
+  tv = (glob == 0);
+  f();
+  
+  __asm__("nop": "=x"(glob): "x="(glob));
+
+  if (tv)
+    __goblint_assert(glob == 0); //UNKNOWN
+  else 
+    __goblint_assert(glob != 0); //UNKNOWN
+
+}
+
diff --git a/tests/regression/79-assembly/28-asm_deadlock.c b/tests/regression/79-assembly/10-asm-deadlock.c
similarity index 100%
rename from tests/regression/79-assembly/28-asm_deadlock.c
rename to tests/regression/79-assembly/10-asm-deadlock.c
diff --git a/tests/regression/79-assembly/32-asm-mem-leak.c b/tests/regression/79-assembly/11-asm-mem-leak.c
similarity index 100%
rename from tests/regression/79-assembly/32-asm-mem-leak.c
rename to tests/regression/79-assembly/11-asm-mem-leak.c
diff --git a/tests/regression/79-assembly/55-asm-taint b/tests/regression/79-assembly/12-asm-taint.c
similarity index 90%
rename from tests/regression/79-assembly/55-asm-taint
rename to tests/regression/79-assembly/12-asm-taint.c
index 0a8b40e718..cfdcf146a3 100644
--- a/tests/regression/79-assembly/55-asm-taint
+++ b/tests/regression/79-assembly/12-asm-taint.c
@@ -1,4 +1,4 @@
-//PARAM --set "ana.activated[+]" taintPartialContexts --set ana.ctx_insens[+] base
+//PARAM --set "ana.activated[+]" taintPartialContexts --set ana.ctx_insens[+] base --disable asm_is_nop
 #include <goblint.h>
 
 
diff --git a/tests/regression/79-assembly/57-jmpbuf-invalid.c b/tests/regression/79-assembly/13-jmpbuf-invalid.c
similarity index 100%
rename from tests/regression/79-assembly/57-jmpbuf-invalid.c
rename to tests/regression/79-assembly/13-jmpbuf-invalid.c
diff --git a/tests/regression/79-assembly/58-asm-region b/tests/regression/79-assembly/14-asm-region.c
similarity index 100%
rename from tests/regression/79-assembly/58-asm-region
rename to tests/regression/79-assembly/14-asm-region.c
diff --git a/tests/regression/79-assembly/15-jumpbuf-poison.c b/tests/regression/79-assembly/15-jumpbuf-poison.c
new file mode 100644
index 0000000000..e44474611f
--- /dev/null
+++ b/tests/regression/79-assembly/15-jumpbuf-poison.c
@@ -0,0 +1,25 @@
+// PARAM: --disable asm_is_nop
+#include <stdio.h>
+#include <setjmp.h>
+
+jmp_buf buf;
+
+void test(void) {
+
+	longjmp(buf, 1);
+}
+
+int main(void) {
+
+	int i = 0;
+
+	if (setjmp(buf)){
+	
+		printf("After Jump: %d\n",i); //WARN
+	} else {
+	
+		printf("Setting i to 69; %d\n", i);
+		asm ("nop" : "=x"(i) : "=x"(i));
+		test();
+	}
+}
diff --git a/tests/regression/79-assembly/16-jumpbuf-read-poison.c b/tests/regression/79-assembly/16-jumpbuf-read-poison.c
new file mode 100644
index 0000000000..8f409bf1de
--- /dev/null
+++ b/tests/regression/79-assembly/16-jumpbuf-read-poison.c
@@ -0,0 +1,25 @@
+// PARAM: --disable asm_is_nop
+#include <stdio.h>
+#include <setjmp.h>
+
+jmp_buf buf;
+
+void test(void) {
+
+	longjmp(buf, 1);
+}
+
+int main(void) {
+
+	int i = 0;
+
+	if (setjmp(buf)){
+	
+		asm ("nop" : "x="(i):"x="(i)); //WARN
+	} else {
+	
+		printf("Setting i to 69; %d\n", i);
+		i = 10;
+		test();
+	}
+}