From bb69ca8464e84f3ae1f67a8cabcf3793f359ddfb Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Tue, 19 May 2026 10:17:43 -0400
Subject: [PATCH] LLVM/MIR: Use the same pretty-printer consistently in
 structural mismatch errors

This should minimize some spurious differences in expected/actual when
displaying structural mismatch errors arising from overrides. Still not perfect
by any means, but an improvement nonetheless.
---
 .../src/SAWCentral/Crucible/LLVM/Override.hs  | 19 +++++++++----------
 .../src/SAWCentral/Crucible/MIR/Override.hs   |  9 ++++-----
 2 files changed, 13 insertions(+), 15 deletions(-)

diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/Override.hs b/saw-central/src/SAWCentral/Crucible/LLVM/Override.hs
index e44fc91eb2..bf149a0027 100644
--- a/saw-central/src/SAWCentral/Crucible/LLVM/Override.hs
+++ b/saw-central/src/SAWCentral/Crucible/LLVM/Override.hs
@@ -163,23 +163,22 @@ prettySetupValueAsLLVMVal opts cc spec setupval = do
 -- | Try to translate the spec\'s 'SetupValue' into an 'LLVMVal', pretty-print
 --   the 'LLVMVal'.
 mkStructuralMismatch ::
-  (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
+  (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
   Options              {- ^ output/verbosity options -} ->
   LLVMCrucibleContext arch ->
-  SharedContext {- ^ context for constructing SAW terms -} ->
   MS.CrucibleMethodSpecIR (LLVM arch) {- ^ for name and typing environments -} ->
   Crucible.LLVMVal Sym {- ^ the value from the simulator -} ->
   SetupValue (LLVM arch)           {- ^ the value from the spec -} ->
   Crucible.MemType     {- ^ the expected type -} ->
   OverrideMatcher (LLVM arch) w (OverrideFailureReason (LLVM arch))
-mkStructuralMismatch _opts cc sc spec llvmval setupval memTy = do
+mkStructuralMismatch opts cc spec llvmval setupval memTy = do
   let tyEnv = MS.csAllocations spec
       nameEnv = MS.csTypeNames spec
       maybeMsgTy = either (const Nothing) Just $ runExcept (typeOfSetupValue cc tyEnv nameEnv setupval)
-  setupval' <- liftIO $ MS.prettySetupValue sc setupval
+  setupval' <- resolveSetupValueLLVM opts cc spec setupval
   pure $ StructuralMismatch
               (PP.pretty llvmval)
-              setupval'
+              (PP.pretty setupval')
               maybeMsgTy
               memTy
 
@@ -1168,7 +1167,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected =
     (_, _, SetupTerm expectedTT)
       | TypedTermSchema (Cryptol.Forall [] [] tyexpr) <- ttType expectedTT
       , Right tval <- Cryptol.evalType mempty tyexpr
-        -> do failMsg  <- mkStructuralMismatch opts cc sc cs actual expected expectedTy
+        -> do failMsg  <- mkStructuralMismatch opts cc cs actual expected expectedTy
               realTerm <- valueToSC sym md failMsg tval actual
               instantiateExtMatchTerm sc md prepost realTerm (ttTerm expectedTT)
 
@@ -1242,13 +1241,13 @@ matchArg opts sc cc cs prepost md actual expectedTy expected =
 
         _ -> do
             ppopts <- liftIO $ scGetPPOpts sc
-            err <- mkStructuralMismatch opts cc sc cs actual expected expectedTy
+            err <- mkStructuralMismatch opts cc cs actual expected expectedTy
             failure ppopts loc err
-              
+
 
     _ -> do
         ppopts <- liftIO $ scGetPPOpts sc
-        err <- mkStructuralMismatch opts cc sc cs actual expected expectedTy
+        err <- mkStructuralMismatch opts cc cs actual expected expectedTy
         failure ppopts loc err
 
   where
@@ -1260,7 +1259,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected =
       if diffMemTypes expectedTy ty /= []
       then do
           ppopts <- liftIO $ scGetPPOpts sc
-          err <- mkStructuralMismatch opts cc sc cs actual expected expectedTy
+          err <- mkStructuralMismatch opts cc cs actual expected expectedTy
           failure ppopts loc err
       else liftIO (Crucible.testEqual sym val actual) >>=
         \case
diff --git a/saw-central/src/SAWCentral/Crucible/MIR/Override.hs b/saw-central/src/SAWCentral/Crucible/MIR/Override.hs
index 3bd22471b9..0719b9772b 100644
--- a/saw-central/src/SAWCentral/Crucible/MIR/Override.hs
+++ b/saw-central/src/SAWCentral/Crucible/MIR/Override.hs
@@ -1665,7 +1665,7 @@ matchArg opts sc cc cs prepost md = go False []
 
       structuralMismatch :: OverrideMatcher MIR w (OverrideFailureReason MIR)
       structuralMismatch =
-        mkStructuralMismatch opts cc sc cs actual
+        mkStructuralMismatch opts cc cs actual
           (reapplyProjToSetupValue projStack expected)
 
       tryMirOperation :: MatchAssertM w a -> OverrideMatcher MIR w a
@@ -2025,18 +2025,17 @@ methodSpecHandler_prestate opts sc cc args cs =
 mkStructuralMismatch ::
   Options              {- ^ output/verbosity options -} ->
   MIRCrucibleContext ->
-  SharedContext {- ^ context for constructing SAW terms -} ->
   CrucibleMethodSpecIR {- ^ for name and typing environments -} ->
   MIRVal {- ^ the value from the simulator -} ->
   SetupValue {- ^ the value from the spec -} ->
   OverrideMatcher MIR w (OverrideFailureReason MIR)
-mkStructuralMismatch _opts cc sc spec mirVal@(MIRVal shp _) setupval = do
+mkStructuralMismatch opts cc spec mirVal@(MIRVal shp _) setupval = do
   let sym = cc^.mccSym
   setupTy <- typeOfSetupValueMIR cc spec setupval
-  setupval' <- liftIO $ MS.prettySetupValue sc setupval
+  setupval' <- resolveSetupValueMIR opts cc spec setupval
   pure $ StructuralMismatch
             (prettyMIRVal sym mirVal)
-            setupval'
+            (prettyMIRVal sym setupval')
             (Just setupTy)
             (shapeMirTy shp)