From 0e315257dc48b4e95c4a75528b2e8653ce07232d Mon Sep 17 00:00:00 2001
From: Benjamin Bott <benjamin.bott@tum.de>
Date: Sun, 1 May 2022 21:16:00 +0200
Subject: [PATCH] Invalidate variables (potentially) modified by an asm
 statement

---
 src/analyses/base.ml                          | 20 ++++++++++++
 src/util/options.schema.json                  | 32 +++++++++++++++++++
 tests/regression/56-asm/01-parsing.c          | 14 ++++++++
 .../56-asm/02-basic-discard-local.c           | 12 +++++++
 .../56-asm/03-basic-discard-global.c          | 12 +++++++
 tests/regression/56-asm/04-memory-clobber.c   | 12 +++++++
 .../56-asm/10-advanced-discard-local.c        | 15 +++++++++
 .../56-asm/11-advanced-discard-global.c       | 15 +++++++++
 .../56-asm/12-advanced-discard-mixed.c        | 20 ++++++++++++
 .../56-asm/13-advanced-discard-local-multi.c  | 17 ++++++++++
 .../56-asm/14-advanced-discard-global-multi.c | 17 ++++++++++
 .../56-asm/15-advanced-discard-mixed-multi.c  | 24 ++++++++++++++
 .../56-asm/20-advanced-read-local.c           | 16 ++++++++++
 .../56-asm/21-advanced-read-global.c          | 16 ++++++++++
 .../56-asm/22-advanced-read-mixed.c           | 21 ++++++++++++
 .../56-asm/23-advanced-read-local-multi.c     | 18 +++++++++++
 .../56-asm/24-advanced-read-global-multi.c    | 18 +++++++++++
 .../56-asm/25-advanced-read-mixed-multi.c     | 25 +++++++++++++++
 tests/regression/56-asm/30-simple-branch.c    | 17 ++++++++++
 tests/regression/56-asm/31-struct-value.c     | 19 +++++++++++
 .../56-asm/32-struct-value-branch.c           | 22 +++++++++++++
 tests/regression/56-asm/33-struct-ptr.c       | 26 +++++++++++++++
 tests/regression/56-asm/34-struct-pr-branch.c | 29 +++++++++++++++++
 23 files changed, 437 insertions(+)
 create mode 100644 tests/regression/56-asm/01-parsing.c
 create mode 100644 tests/regression/56-asm/02-basic-discard-local.c
 create mode 100644 tests/regression/56-asm/03-basic-discard-global.c
 create mode 100644 tests/regression/56-asm/04-memory-clobber.c
 create mode 100644 tests/regression/56-asm/10-advanced-discard-local.c
 create mode 100644 tests/regression/56-asm/11-advanced-discard-global.c
 create mode 100644 tests/regression/56-asm/12-advanced-discard-mixed.c
 create mode 100644 tests/regression/56-asm/13-advanced-discard-local-multi.c
 create mode 100644 tests/regression/56-asm/14-advanced-discard-global-multi.c
 create mode 100644 tests/regression/56-asm/15-advanced-discard-mixed-multi.c
 create mode 100644 tests/regression/56-asm/20-advanced-read-local.c
 create mode 100644 tests/regression/56-asm/21-advanced-read-global.c
 create mode 100644 tests/regression/56-asm/22-advanced-read-mixed.c
 create mode 100644 tests/regression/56-asm/23-advanced-read-local-multi.c
 create mode 100644 tests/regression/56-asm/24-advanced-read-global-multi.c
 create mode 100644 tests/regression/56-asm/25-advanced-read-mixed-multi.c
 create mode 100644 tests/regression/56-asm/30-simple-branch.c
 create mode 100644 tests/regression/56-asm/31-struct-value.c
 create mode 100644 tests/regression/56-asm/32-struct-value-branch.c
 create mode 100644 tests/regression/56-asm/33-struct-ptr.c
 create mode 100644 tests/regression/56-asm/34-struct-pr-branch.c

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 20f886b7e5e..151b12bec72 100644
--- a/src/analyses/base.ml
+++ b/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
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index e8b6cb1731b..03ebf3e2ed9 100644
--- a/src/util/options.schema.json
+++ b/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
diff --git a/tests/regression/56-asm/01-parsing.c b/tests/regression/56-asm/01-parsing.c
new file mode 100644
index 00000000000..bb055469121
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/02-basic-discard-local.c b/tests/regression/56-asm/02-basic-discard-local.c
new file mode 100644
index 00000000000..0914212512b
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/03-basic-discard-global.c b/tests/regression/56-asm/03-basic-discard-global.c
new file mode 100644
index 00000000000..454fd8956e7
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/04-memory-clobber.c b/tests/regression/56-asm/04-memory-clobber.c
new file mode 100644
index 00000000000..59673cfbf3d
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/10-advanced-discard-local.c b/tests/regression/56-asm/10-advanced-discard-local.c
new file mode 100644
index 00000000000..fb6e4685fa5
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/11-advanced-discard-global.c b/tests/regression/56-asm/11-advanced-discard-global.c
new file mode 100644
index 00000000000..f870974e7ae
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/12-advanced-discard-mixed.c b/tests/regression/56-asm/12-advanced-discard-mixed.c
new file mode 100644
index 00000000000..fe8609a672a
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/13-advanced-discard-local-multi.c b/tests/regression/56-asm/13-advanced-discard-local-multi.c
new file mode 100644
index 00000000000..82ab281ff45
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/14-advanced-discard-global-multi.c b/tests/regression/56-asm/14-advanced-discard-global-multi.c
new file mode 100644
index 00000000000..b6c52cbb1ff
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/15-advanced-discard-mixed-multi.c b/tests/regression/56-asm/15-advanced-discard-mixed-multi.c
new file mode 100644
index 00000000000..8ecd451d89e
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/20-advanced-read-local.c b/tests/regression/56-asm/20-advanced-read-local.c
new file mode 100644
index 00000000000..d8b7b33a148
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/21-advanced-read-global.c b/tests/regression/56-asm/21-advanced-read-global.c
new file mode 100644
index 00000000000..d5efabd86ff
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/22-advanced-read-mixed.c b/tests/regression/56-asm/22-advanced-read-mixed.c
new file mode 100644
index 00000000000..684c1bc5148
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/23-advanced-read-local-multi.c b/tests/regression/56-asm/23-advanced-read-local-multi.c
new file mode 100644
index 00000000000..e3d4528bb0b
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/24-advanced-read-global-multi.c b/tests/regression/56-asm/24-advanced-read-global-multi.c
new file mode 100644
index 00000000000..9cb433c0055
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/25-advanced-read-mixed-multi.c b/tests/regression/56-asm/25-advanced-read-mixed-multi.c
new file mode 100644
index 00000000000..d174c59a3bf
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/30-simple-branch.c b/tests/regression/56-asm/30-simple-branch.c
new file mode 100644
index 00000000000..60153fc7b15
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/31-struct-value.c b/tests/regression/56-asm/31-struct-value.c
new file mode 100644
index 00000000000..16ddfc49660
--- /dev/null
+++ b/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;
+}
diff --git a/tests/regression/56-asm/32-struct-value-branch.c b/tests/regression/56-asm/32-struct-value-branch.c
new file mode 100644
index 00000000000..56f6dc74f7b
--- /dev/null
+++ b/tests/regression/56-asm/32-struct-value-branch.c
@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int main()
+{
+  struct test
+  {
+    int a;
+    int b;
+  } x = {0, 0};
+  int y;
+
+  if (!y)
+  {
+    asm("movl $1, %0"
+        : "=r"(x.a));
+  }
+
+  assert(x.a == 1); // UNKNOWN
+  assert(x.b == 0);
+
+  return 0;
+}
diff --git a/tests/regression/56-asm/33-struct-ptr.c b/tests/regression/56-asm/33-struct-ptr.c
new file mode 100644
index 00000000000..bdd28174c4f
--- /dev/null
+++ b/tests/regression/56-asm/33-struct-ptr.c
@@ -0,0 +1,26 @@
+#include <assert.h>
+
+int main()
+{
+  struct test
+  {
+    int a;
+    int b;
+  };
+
+  struct test v = {0, 0};
+  struct test *x = &v;
+  int y;
+
+  asm("nop"
+      :
+      : "r"(x));
+
+  assert(x->a == 0); // UNKNOWN
+  assert(x->b == 0); // UNKNOWN
+
+  assert(v.a == 0); // UNKNOWN
+  assert(v.b == 0); // UNKNOWN
+
+  return 0;
+}
diff --git a/tests/regression/56-asm/34-struct-pr-branch.c b/tests/regression/56-asm/34-struct-pr-branch.c
new file mode 100644
index 00000000000..9bb0ba05f1c
--- /dev/null
+++ b/tests/regression/56-asm/34-struct-pr-branch.c
@@ -0,0 +1,29 @@
+#include <assert.h>
+
+int main()
+{
+  struct test
+  {
+    int a;
+    int b;
+  };
+
+  struct test v = {0, 0};
+  struct test *x = &v;
+  int y;
+
+  if (!y)
+  {
+    asm("nop"
+        :
+        : "r"(x));
+  }
+
+  assert(x->a == 0); // UNKNOWN
+  assert(x->b == 0); // UNKNOWN
+
+  assert(v.a == 0); // UNKNOWN
+  assert(v.b == 0); // UNKNOWN
+
+  return 0;
+}