tests

Author: Simon Tietz

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;

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;

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;

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;

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;

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

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;
+}

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!");
+}

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;
+}