x86: Pass the right nameEnv in resolvePtrSetupValue

Previously, `resolvePtrSetupValue` would pass an empty `Map` of `Ident` to
`resolveSetupVal`, which prevented SAW from lookup up struct field names
properly. The fix is quite straightforward, luckily enough.

Fixes #1533.

.gitignore

@@ -24,6 +24,7 @@ intTests/test_intro_examples/*.cnf
 intTests/test_llvm_x86_0[1234]/test
 intTests/test_llvm_x86_0[1234]/test.o
 intTests/test_llvm_x86_0[1234]/test.bc
+intTests/test1533/test.o
 intTests/test*/*.out
 intTests/test_crucible_jvm/Stat.class
 intTests/test_profiling/prof

intTests/test1533/Makefile

@@ -0,0 +1,17 @@
+CC = clang
+CFLAGS = -g -frecord-command-line -O0
+
+all: test.bc test.exe
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c -emit-llvm $< -o $@
+
+test.o: test.c
+	$(CC) $(CFLAGS) -c $< -o $@
+
+test.exe: test.o
+	$(CC) $(CFLAGS) $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc test.exe

intTests/test1533/test.c

@@ -0,0 +1,14 @@
+#include <stdint.h>
+
+struct s {
+  uint8_t x1;
+  uint8_t x2;
+};
+
+uint8_t get_x2(struct s *ss) {
+  return ss->x2;
+}
+
+int main() {
+  return 0;
+}

intTests/test1533/test.saw

@@ -0,0 +1,14 @@
+enable_experimental;
+
+let get_x2_spec = do {
+  ss <- llvm_alloc (llvm_alias "struct.s");
+  z <- llvm_fresh_var "z" (llvm_int 8);
+  llvm_points_to (llvm_field ss "x2") (llvm_term z);
+  llvm_execute_func [ss];
+  llvm_return (llvm_term z);
+};
+
+m <- llvm_load_module "test.bc";
+
+llvm_verify     m            "get_x2" [] false get_x2_spec (w4_unint_z3 []);
+llvm_verify_x86 m "test.exe" "get_x2" [] false get_x2_spec (w4_unint_z3 []);

intTests/test1533/test.sh

@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+
+set -e
+
+$SAW test.saw

src/SAWScript/Crucible/LLVM/X86.hs

@@ -762,7 +762,7 @@ assumePointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tptval) = do
   opts <- use x86Options
   cc <- use x86CrucibleContext
   mem <- use x86Mem
-  ptr <- resolvePtrSetupValue env tyenv tptr
+  ptr <- resolvePtrSetupValue env tyenv nameEnv tptr
   cond' <- liftIO $ mapM (resolveSAWPred cc . ttTerm) cond
   mem' <- liftIO $ LO.storePointsToValue opts cc env tyenv nameEnv mem cond' ptr tptval Nothing
   x86Mem .= mem'
@@ -771,9 +771,10 @@ resolvePtrSetupValue ::
   X86Constraints =>
   Map MS.AllocIndex Ptr ->
   Map MS.AllocIndex LLVMAllocSpec ->
+  Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} ->
   MS.SetupValue LLVM ->
   X86Sim Ptr
-resolvePtrSetupValue env tyenv tptr = do
+resolvePtrSetupValue env tyenv nameEnv tptr = do
   sym <- use x86Sym
   cc <- use x86CrucibleContext
   mem <- use x86Mem
@@ -789,7 +790,7 @@ resolvePtrSetupValue env tyenv tptr = do
         let addr = fromIntegral $ Elf.steValue entry
         liftIO $ C.LLVM.doPtrAddOffset sym mem base =<< W4.bvLit sym knownNat (BV.mkBV knownNat addr)
     _ -> liftIO $ C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64)
-         =<< resolveSetupVal cc mem env tyenv Map.empty tptr
+         =<< resolveSetupVal cc mem env tyenv nameEnv tptr
 
 -- | Write each SetupValue passed to llvm_execute_func to the appropriate
 -- x86_64 register from the calling convention.
@@ -852,6 +853,7 @@ assertPost globals env premem preregs = do
   postregs <- use x86Regs
   let
     tyenv = ms ^. MS.csPreState . MS.csAllocs
+    nameEnv = MS.csTypeNames ms
 
   prersp <- getReg Macaw.RSP preregs
   expectedIP <- liftIO $ C.LLVM.doLoad sym premem prersp (C.LLVM.bitvectorType 8)
@@ -890,7 +892,7 @@ assertPost globals env premem preregs = do
 
 
   pointsToMatches <- forM (ms ^. MS.csPostState . MS.csPointsTos)
-    $ assertPointsTo env tyenv
+    $ assertPointsTo env tyenv nameEnv
 
   let setupConditionMatchesPre = fmap -- assume preconditions
         (LO.executeSetupCondition opts sc cc ms)
@@ -931,15 +933,16 @@ assertPointsTo ::
   X86Constraints =>
   Map MS.AllocIndex Ptr {- ^ Associates each AllocIndex with the corresponding allocation -} ->
   Map MS.AllocIndex LLVMAllocSpec {- ^ Associates each AllocIndex with its specification -} ->
+  Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} ->
   LLVMPointsTo LLVMArch {- ^ llvm_points_to statement from the precondition -} ->
   X86Sim (LLVMOverrideMatcher md ())
-assertPointsTo env tyenv pointsTo@(LLVMPointsTo loc cond tptr tptval) = do
+assertPointsTo env tyenv nameEnv pointsTo@(LLVMPointsTo loc cond tptr tptval) = do
   opts <- use x86Options
   sc <- use x86SharedContext
   cc <- use x86CrucibleContext
   ms <- use x86MethodSpec
 
-  ptr <- resolvePtrSetupValue env tyenv tptr
+  ptr <- resolvePtrSetupValue env tyenv nameEnv tptr
   pure $ do
     err <- LO.matchPointsToValue opts sc cc ms MS.PostState loc cond ptr tptval
     case err of