Relax disjoint check for globals and fresh pointers. (#1858)

* Relax disjoint check for globals and fresh pointers.

* Add test.

* Address comments.

Author: andreistefanescu

intTests/test_llvm_global_fresh_pointer/Makefile

@@ -0,0 +1,11 @@
+CLANG ?= clang
+CFLAGS = -g -frecord-command-line
+
+all: test.bc
+
+test.bc: test.c
+	$(CLANG) -c -emit-llvm $(CFLAGS) $< -o $@
+
+clean:
+	rm -f test.bc
+

intTests/test_llvm_global_fresh_pointer/test.bc

@@ -0,0 +1,8 @@
+int glb;
+
+void foo(const int *x) {}
+
+void bar(const int *x) {
+  foo(x);
+}
+

intTests/test_llvm_global_fresh_pointer/test.c

@@ -0,0 +1,30 @@
+enable_experimental;
+
+m <- llvm_load_module "test.bc";
+
+// test the fact that glb and x_ptr are allowed to alias each other.
+let foo_spec = do {
+  llvm_alloc_global "glb";
+  x_ptr <- llvm_fresh_pointer (llvm_int 32);
+
+  llvm_execute_func [x_ptr];
+};
+  
+foo_ov <- llvm_verify m "foo"
+  []
+  false
+  foo_spec
+  (do {
+    print_goal;
+    w4_unint_z3 [];
+  });
+
+llvm_verify m "bar"
+  [foo_ov]
+  false
+  foo_spec
+  (do {
+    print_goal;
+    w4_unint_z3 [];
+  });
+

intTests/test_llvm_global_fresh_pointer/test.saw

@@ -0,0 +1,4 @@
+set -e
+
+$SAW test.saw
+

intTests/test_llvm_global_fresh_pointer/test.sh

@@ -1044,8 +1044,11 @@ enforceDisjointAllocGlobal ::
   (LLVMAllocGlobal arch, LLVMPtr (Crucible.ArchWidth arch)) ->
   OverrideMatcher (LLVM arch) md ()
 enforceDisjointAllocGlobal sym loc
-  (LLVMAllocSpec _pmut _pty _palign psz pMd _pfresh _p_sym_init, p)
-  (LLVMAllocGlobal qloc (L.Symbol qname), q) =
+  (LLVMAllocSpec _pmut _pty _palign psz pMd pfresh _p_sym_init, p)
+  (LLVMAllocGlobal qloc (L.Symbol qname), q)
+  | pfresh =
+    pure () -- Fresh pointers need not be disjoint
+  | otherwise =
   do let Crucible.LLVMPointer pblk _ = p
      let Crucible.LLVMPointer qblk _ = q
      c <- liftIO $ W4.notPred sym =<< W4.natEq sym pblk qblk