Invalidate variables (potentially) modified by an asm statement

src/analyses/base.ml

@@ -2401,6 +2401,26 @@ struct
     (* D.join ctx.local @@ *)
     ctx.local
 
+  let asm ctx =
+    let inv_globs, inv_exps = match ctx.edge with
+      | (MyCFG.ASM (_, None)) ->
+        (* asm basic instruction *)
+        (not (get_bool "sem.asm.basic-preserve-globals"), [])
+      | MyCFG.ASM (_, Some (outs, ins, clobbers)) ->
+        (* advanced asm instructions *)
+        (
+          List.mem "memory" clobbers && not (get_bool "sem.asm.memory-preserve-globals"),
+          List.append (if get_bool "sem.asm.readonly-inputs" then [] else List.map (fun (_, _, exp) -> exp, InvalidateTransitive) ins)
+            (List.map (fun (_, c, lval) -> Lval lval, match String.find c "+" with 
+               | _ -> InvalidateSelfAndTransitive
+               | exception Not_found -> InvalidateSelf) outs)
+        )
+      | _ ->
+        (* not an asm instruction at all ?? *)
+        (false, []) in
+    (if get_bool "sem.asm.enabled" then invalidate_core ~ctx inv_globs inv_exps);
+    ctx.local
+
   let event ctx e octx =
     let st: store = ctx.local in
     let ask = ask_of_ctx ctx in

src/util/options.schema.json

@@ -1108,6 +1108,38 @@
             }
           },
           "additionalProperties": false
+        },
+        "asm": {
+          "title": "sem.asm",
+          "description": "Inline Assembly Analysis options",
+          "type": "object",
+          "properties": {
+            "enabled": {
+              "title": "sem.asm.enabled",
+              "description": "",
+              "type": "boolean",
+              "default": true
+            },
+            "basic-preserve-globals": {
+              "title": "sem.asm.basic-preserve-globals",
+              "description": "If enabled, do preserve globals across basic asm statements",
+              "type": "boolean",
+              "default": false
+            },
+            "memory-preserve-globals": {
+              "title": "sem.asm.memory-preserve-globals",
+              "description": "If enabled, do preserve globals across advanced asm statements with memory clobber annotation",
+              "type": "boolean",
+              "default": false
+            },
+            "readonly-inputs": {
+              "title": "sem.asm.readonly-inputs",
+              "description": "If enabled, do not consider changes through pointers given as inputs",
+              "type": "boolean",
+              "default": false
+            }
+          },
+          "additionalProperties": false
         }
       },
       "additionalProperties": false

tests/regression/56-asm/01-parsing.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int x;
+
+  asm("nop");
+
+  asm volatile("");
+
+  assert(1);
+
+  return 0;
+}

tests/regression/56-asm/02-basic-discard-local.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int main()
+{
+  int x = 0;
+
+  asm("nop");
+
+  assert(x == 0);
+
+  return 0;
+}

tests/regression/56-asm/03-basic-discard-global.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int x = 0;
+
+int main()
+{
+  asm("nop");
+
+  assert(x == 0); // UNKNOWN
+
+  return 0;
+}

tests/regression/56-asm/04-memory-clobber.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int x = 0;
+
+int main()
+{
+  asm("movl $1, x" : : : "memory");
+
+  assert(x == 1); // UNKNOWN
+
+  return 0;
+}

tests/regression/56-asm/10-advanced-discard-local.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int main()
+{
+  int x = 0;
+  int y = 0;
+
+  asm("nop"
+      : "=r"(x));
+
+  assert(x == 0); // UNKNOWN
+  assert(y == 0);
+
+  return 0;
+}

tests/regression/56-asm/11-advanced-discard-global.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int x = 0;
+int y = 0;
+
+int main()
+{
+  asm("nop"
+      : "=r"(x));
+
+  assert(x == 0); // UNKNOWN
+  assert(y == 0);
+
+  return 0;
+}

tests/regression/56-asm/12-advanced-discard-mixed.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+int gx = 0;
+int gy = 0;
+
+int main()
+{
+  int x = 0;
+  int y = 0;
+
+  asm("nop"
+      : "=r"(x), "=r"(gx));
+
+  assert(x == 0); // UNKNOWN
+  assert(y == 0);
+  assert(gx == 0); // UNKNOWN
+  assert(gy == 0);
+
+  return 0;
+}

tests/regression/56-asm/13-advanced-discard-local-multi.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main()
+{
+  int x = 0;
+  int y = 0;
+  int z = 0;
+
+  asm("nop"
+      : "=r"(x), "=r"(y));
+
+  assert(x == 0); // UNKNOWN
+  assert(y == 0); // UNKNOWN
+  assert(z == 0);
+
+  return 0;
+}

tests/regression/56-asm/14-advanced-discard-global-multi.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int x = 0;
+int y = 0;
+int z = 0;
+
+int main()
+{
+  asm("nop"
+      : "=r"(x), "=r"(y));
+
+  assert(x == 0); // UNKNOWN
+  assert(y == 0); // UNKNOWN
+  assert(z == 0);
+
+  return 0;
+}

tests/regression/56-asm/15-advanced-discard-mixed-multi.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+int gx = 0;
+int gy = 0;
+int gz = 0;
+
+int main()
+{
+  int x = 0;
+  int y = 0;
+  int z = 0;
+
+  asm("nop"
+      : "=r"(x), "=r"(y), "=r"(gx), "=r"(gy));
+
+  assert(x == 0); // UNKNOWN
+  assert(y == 0); // UNKNOWN
+  assert(z == 0);
+  assert(gx == 0); // UNKNOWN
+  assert(gy == 0); // UNKNOWN
+  assert(gz == 0);
+
+  return 0;
+}

tests/regression/56-asm/20-advanced-read-local.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int main()
+{
+  int x = 0;
+  int y = 0;
+
+  asm("nop"
+      :
+      : "r"(x));
+
+  assert(x == 0);
+  assert(y == 0);
+
+  return 0;
+}

tests/regression/56-asm/21-advanced-read-global.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int x = 0;
+int y = 0;
+
+int main()
+{
+  asm("nop"
+      :
+      : "r"(x));
+
+  assert(x == 0);
+  assert(y == 0);
+
+  return 0;
+}

tests/regression/56-asm/22-advanced-read-mixed.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+
+int gx = 0;
+int gy = 0;
+
+int main()
+{
+  int x = 0;
+  int y = 0;
+
+  asm("nop"
+      :
+      : "r"(x), "r"(gx));
+
+  assert(x == 0);
+  assert(y == 0);
+  assert(gx == 0);
+  assert(gy == 0);
+
+  return 0;
+}

tests/regression/56-asm/23-advanced-read-local-multi.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+int main()
+{
+  int x = 0;
+  int y = 0;
+  int z = 0;
+
+  asm("nop"
+      :
+      : "r"(x), "r"(y));
+
+  assert(x == 0);
+  assert(y == 0);
+  assert(z == 0);
+
+  return 0;
+}

tests/regression/56-asm/24-advanced-read-global-multi.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+int x = 0;
+int y = 0;
+int z = 0;
+
+int main()
+{
+  asm("nop"
+      :
+      : "r"(x), "r"(y));
+
+  assert(x == 0);
+  assert(y == 0);
+  assert(z == 0);
+
+  return 0;
+}

tests/regression/56-asm/25-advanced-read-mixed-multi.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+
+int gx = 0;
+int gy = 0;
+int gz = 0;
+
+int main()
+{
+  int x = 0;
+  int y = 0;
+  int z = 0;
+
+  asm("nop"
+      :
+      : "r"(x), "r"(y), "r"(gx), "r"(gy));
+
+  assert(x == 0);
+  assert(y == 0);
+  assert(z == 0);
+  assert(gx == 0);
+  assert(gy == 0);
+  assert(gz == 0);
+
+  return 0;
+}

tests/regression/56-asm/30-simple-branch.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main()
+{
+  int x = 0;
+  int y;
+
+  if (!y)
+  {
+    asm("movl $1, %0"
+        : "=r"(x));
+  }
+
+  assert(x == 1); // UNKNOWN
+
+  return 0;
+}

tests/regression/56-asm/31-struct-value.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int main()
+{
+  struct test
+  {
+    int a;
+    int b;
+  } x = {0, 0};
+  int y;
+
+  asm("movl $1, %0"
+      : "=r"(x.a));
+
+  assert(x.a == 1); // UNKNOWN
+  assert(x.b == 0);
+
+  return 0;
+}