macaw-symbolic: Implement MacawFreshSymbolic for all macaw Types

Rather than `error`ing, we now generate fresh constants for all possible
`macaw` `Type`s that are supplied to the `MacawFreshSymbolic` operation.

Fixes #301.

macaw-aarch32-symbolic/tests/pass/Makefile

@@ -25,6 +25,12 @@ movt.unopt.exe: movt.c
 movt.opt.exe: movt.c
 	$(CC) $(CFLAGS) -mcpu=cortex-a7 -O2 $< -o $@
 
+# We need to pass -mcpu=cortex-a7 here
+strd.unopt.exe: strd.s
+	$(CC) $(CFLAGS) -mcpu=cortex-a7 -O0 $< -o $@
+strd.opt.exe: strd.s
+	$(CC) $(CFLAGS) -mcpu=cortex-a7 -O2 $< -o $@
+
 so/libfib.unopt.so: so/fib.c so/libgetone.unopt.so
 	$(CC) $(SO_CFLAGS) -O0 -Lso/ -Iso/ -shared $< -lgetone.unopt -o $@
 so/libfib.opt.so: so/fib.c so/libgetone.opt.so

macaw-aarch32-symbolic/tests/pass/strd.c_template

@@ -0,0 +1,18 @@
+// In Ubuntu 20.04, compiling this C code will result in the assembly code in
+// strd.s. Sadly, Ubuntu 22.04's version of gcc will produce slightly different
+// assembly that does not include the strd instruction, which is critical for
+// testing the issue in https://github.com/GaloisInc/macaw/issues/301. As such,
+// I've checked in the assembly code to ensure that we can continue testing code
+// involving strd, but I've also checked in the original C code as a reference.
+#include <stdint.h>
+
+uint64_t x = 0;
+
+int __attribute__((noinline)) test_strd() {
+  x = 42;
+  return x == 42;
+}
+
+void _start() {
+  test_strd();
+}

macaw-aarch32-symbolic/tests/pass/strd.s

@@ -0,0 +1,31 @@
+  .global test_strd
+  .syntax unified
+test_strd:
+  push    {fp}            @ (str fp, [sp, #-4]!)
+  add     fp, sp, #0
+  movw    r3, #312        @ 0x138
+  movt    r3, #2
+  mov     r0, #42 @ 0x2a
+  mov     r1, #0
+  strd    r0, [r3]
+  movw    r3, #312        @ 0x138
+  movt    r3, #2
+  ldrd    r2, [r3]
+  cmp     r3, #0
+  cmpeq   r2, #42 @ 0x2a
+  moveq   r3, #1
+  movne   r3, #0
+  uxtb    r3, r3
+  mov     r0, r3
+  add     sp, fp, #0
+  pop     {fp}            @ (ldr fp, [sp], #4)
+  bx      lr
+
+  .global _start
+  .syntax unified
+_start:
+  push    {fp, lr}
+  add     fp, sp, #4
+  bl      test_strd
+  nop     {0}
+  pop     {fp, pc}

symbolic/src/Data/Macaw/Symbolic.hs

@@ -162,9 +162,11 @@ import           Data.Parameterized.Some ( Some(Some) )
 import qualified Data.Parameterized.TraversableFC as FC
 import qualified Data.Set as S
 import qualified Data.Text as T
+import qualified Data.Vector as V
 
 import qualified What4.FunctionName as C
 import           What4.Interface
+import           What4.InterpretedFloatingPoint (freshFloatConstant)
 import qualified What4.Utils.StringLiteral as C
 import qualified What4.ProgramLoc as WPL
 
@@ -1234,12 +1236,7 @@ execMacawStmtExtension (SB.MacawArchEvalFn archStmtFn) mvar mmConf s0 st =
       M.addrWidthClass w $ doGetGlobal st mvar globs addr
 
     MacawFreshSymbolic t -> -- XXX: user freshValue
-      do nm <- case userSymbol "macawFresh" of
-                 Right a -> return a
-                 Left err -> fail (show err)
-         v <- case t of
-               M.BoolTypeRepr -> freshConstant sym nm C.BaseBoolRepr
-               _ -> error ("MacawFreshSymbolic: XXX type " ++ show t)
+      do v <- freshCrucibleConstant sym (safeSymbol "macawFresh") t
          return (v,st)
 
     MacawLookupFunctionHandle _ args -> do
@@ -1272,6 +1269,48 @@ execMacawStmtExtension (SB.MacawArchEvalFn archStmtFn) mvar mmConf s0 st =
     MO.LookupSyscallHandle lookupSyscall = lookupSyscallHandle mmConf
     toMemPred = mkGlobalPointerValidityAssertion mmConf
 
+-- | Create a fresh Crucible constant based on the supplied Macaw 'M.TypeRepr'.
+freshCrucibleConstant ::
+  forall sym tp.
+  IsSymInterface sym =>
+  sym ->
+  SolverSymbol ->
+  M.TypeRepr tp ->
+  IO (C.RegValue sym (ToCrucibleType tp))
+freshCrucibleConstant sym nm = go
+  where
+    go :: forall tp'.
+          M.TypeRepr tp' ->
+          IO (C.RegValue sym (ToCrucibleType tp'))
+    go M.BoolTypeRepr =
+      freshConstant sym nm C.BaseBoolRepr
+    go (M.BVTypeRepr w) = do
+      {-
+      We have a choice here of what block number to use. If we want something
+      that can possibly be a pointer, then we must use a symbolic block number.
+      On the other hand, symbolic pointers are often cumbersome in practice,
+      since any read or write to the pointer will possibly alias with any other
+      pointer.
+
+      For this reason, we choose to use block number 0 with a symbolic offset,
+      which gives us a symbolic bitvector that cannot possibly be a pointer.
+      For Macaw's needs, this is probably fine, since Macaw usually overwrites
+      these symbolic values without meaningfully using them. If this choice
+      ever becomes a problem in practice, I have included the code for creating
+      symboic pointers—see "Alternative implementation" below.
+      -}
+      off <- freshConstant sym nm (C.BaseBVRepr w)
+      MM.llvmPointer_bv sym off
+      {- Alternative implementation: -}
+      -- blk <- freshNat sym nm
+      -- off <- freshConstant sym nm (C.BaseBVRepr w)
+      -- pure $ MM.LLVMPointer blk off
+    go (M.FloatTypeRepr fi) =
+      freshFloatConstant sym nm (floatInfoToCrucible fi)
+    go (M.TupleTypeRepr l) = macawListToCrucibleM (fmap C.RV . go) l
+    go (M.VecTypeRepr n tp) =
+      V.replicateM (fromIntegral (natValue n)) (go tp)
+
 -- | Return macaw extension evaluation functions.
 macawExtensions
   :: (IsSymInterface sym, MM.HasLLVMAnn sym, ?memOpts :: MM.MemOptions)