crucible-llvm: Skip llvm.experimental.noalias.scope.decl and llvm.dbg…

….assign (#1205)

This adds `llvm.experimental.noalias.scope.decl` and `llvm.dbg.assign` to the
list of LLVM intrinsics that `crucible-llvm` skips over during simulation.
Doing so unlocks more support for recent LLVM versions.

It is conceivable that we may want to reason about these intrinsics at a deeper level some
day. If so, see:

* #1196 (comment) for
  how this would be done for `llvm.experimental.noalias.scope.decl`
* #1204 (comment) for how
  this would be done for `llvm.dbg.assign`

Fixes #1196. Fixes #1204.

crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs

@@ -1942,6 +1942,8 @@ callFunction defSet instr tailCall_ fnTy fn args assign_f
                  , "llvm.dbg.declare"
                  , "llvm.dbg.addr"
                  , "llvm.dbg.value"
+                 , "llvm.dbg.assign" -- Added in LLVM 16
+                 , "llvm.experimental.noalias.scope.decl" -- Added in LLVM 12
                  , "llvm.lifetime.start"
                  , "llvm.lifetime.start.p0"
                  , "llvm.lifetime.start.p0i8"

crux-llvm/test-data/golden/T1196.c

@@ -0,0 +1,14 @@
+void foo(int* restrict p0, int* restrict p1) {
+	*p0 = *p1;
+}
+
+__attribute__((noinline)) void test_inline_foo(int* p0, int* p1) {
+	foo(p0, p1);
+}
+
+int main(void) {
+    int p0 = 0;
+    int p1 = 1;
+    test_inline_foo(&p0, &p1);
+    return 0;
+}

crux-llvm/test-data/golden/T1196.z3.good

@@ -0,0 +1 @@
+[Crux] Overall status: Valid.

crux-llvm/test-data/golden/T1204.c

@@ -0,0 +1,8 @@
+__attribute__((noinline)) int foo(int x[2]) {
+  return x[0];
+}
+
+int main(void) {
+  int x[2] = { 0, 0 };
+  return foo(x);
+}

crux-llvm/test-data/golden/T1204.z3.good

@@ -0,0 +1 @@
+[Crux] Overall status: Valid.