Fix input ordering isses in Verilog generation

intTests/test_external_abc/test.saw

@@ -38,3 +38,7 @@ write_verilog "write_verilog_seqt.v" seqt;
 // A function that returns a tuple
 let tupt = {{ \(x:[8]) (y:[8]) -> (x + y, x - y) }};
 write_verilog "write_verilog_tupt.v" tupt;
+
+// Check that Verilog counterexamples are in the right order
+sr <- sat w4_abc_verilog {{ \(x:[2][2][8]) -> \(y:[32]) -> y == 0x81050fff /\ x == [[2,3],[4,5]] }};
+caseSatResult sr undefined (\t -> prove_print yices {{ t == ([[0x02,0x03],[0x04,0x05]], 0x81050fff) }});

saw-core-what4/src/Verifier/SAW/Simulator/What4.hs

@@ -870,19 +870,16 @@ w4Solve :: forall sym.
   sym ->
   SharedContext ->
   SATQuery ->
-  IO ([ExtCns Term], [FirstOrderType], [Labeler sym], SBool sym)
+  IO ([(ExtCns Term, (Labeler sym, SValue sym))], SBool sym)
 w4Solve sym sc satq =
   do t <- satQueryAsTerm sc satq
      let varList  = Map.toList (satVariables satq)
-     let argNames = map fst varList
-     let argTys   = map snd varList
      vars <- evalStateT (traverse (traverse (newVarFOT sym)) varList) 0
-     let lbls     = map (fst . snd) vars
      let varMap   = Map.fromList [ (ecVarIndex ec, v) | (ec, (_,v)) <- vars ]
      ref <- newIORef Map.empty
      bval <- w4SolveBasic sym sc mempty varMap ref (satUninterp satq) t
      case bval of
-       VBool v -> return (argNames, argTys, lbls, v)
+       VBool v -> return (vars, v)
        _ -> fail $ "w4Solve: non-boolean result type. " ++ show bval
 
 --
@@ -1060,7 +1057,9 @@ w4EvalAny ::
   SAWCoreState n ->
   SharedContext ->
   Map Ident (SValue (B.ExprBuilder n st fs)) -> Set VarIndex -> Term ->
-  IO ([String], ([Maybe (Labeler (B.ExprBuilder n st fs))], SValue (B.ExprBuilder n st fs)))
+  IO ([String],
+      [SValue (B.ExprBuilder n st fs)],
+      ([Maybe (Labeler (B.ExprBuilder n st fs))], SValue (B.ExprBuilder n st fs)))
 w4EvalAny sym st sc ps unintSet t =
   do modmap <- scGetModuleMap sc
      ref <- newIORef Map.empty
@@ -1088,7 +1087,7 @@ w4EvalAny sym st sc ps unintSet t =
      let vars'' = fmap ready vars
      bval' <- applyAll bval vars''
 
-     return (argNames, (bvs, bval'))
+     return (argNames, vars, (bvs, bval'))
 
 w4Eval ::
   forall n st fs.
@@ -1098,7 +1097,7 @@ w4Eval ::
   Map Ident (SValue (B.ExprBuilder n st fs)) -> Set VarIndex -> Term ->
   IO ([String], ([Maybe (Labeler (B.ExprBuilder n st fs))], SBool (B.ExprBuilder n st fs)))
 w4Eval sym st sc ps uintSet t =
-  do (argNames, (bvs, bval)) <- w4EvalAny sym st sc ps uintSet t
+  do (argNames, _, (bvs, bval)) <- w4EvalAny sym st sc ps uintSet t
      case bval of
        VBool b -> return (argNames, (bvs, b))
        _ -> fail $ "w4Eval: non-boolean result type. " ++ show bval

saw-core/src/Verifier/SAW/FiniteValue.hs

@@ -309,27 +309,41 @@ scFirstOrderValue sc fv =
 
 -- Parsing values from lists of booleans ---------------------------------------
 
-readFiniteValue' :: FiniteType -> S.StateT [Bool] Maybe FiniteValue
-readFiniteValue' ft =
+data Endianness
+  = BigEndian
+  | LittleEndian
+
+readFiniteValue' :: Endianness -> FiniteType -> S.StateT [Bool] Maybe FiniteValue
+readFiniteValue' en ft =
   case ft of
     FTBit      -> do bs <- S.get
                      case bs of
                        []      -> S.lift Nothing
                        b : bs' -> S.put bs' >> return (FVBit b)
-    FTVec n t  -> fvVec t <$> S.replicateM (fromIntegral n) (readFiniteValue' t)
-    FTTuple ts -> FVTuple <$> traverse readFiniteValue' ts
-    FTRec tm   -> FVRec <$> traverse readFiniteValue' tm
+    FTVec n t  -> (fvVec t . fixup) <$> S.replicateM (fromIntegral n) (readFiniteValue' en t)
+                    where fixup = case (t, en) of
+                                    (FTBit, LittleEndian) -> reverse
+                                    _ -> id
+    FTTuple ts -> FVTuple <$> traverse (readFiniteValue' en) ts
+    FTRec tm   -> FVRec <$> traverse (readFiniteValue' en) tm
 
 readFiniteValues :: [FiniteType] -> [Bool] -> Maybe [FiniteValue]
 readFiniteValues ts bs = do
-  (vs, rest) <- S.runStateT (traverse readFiniteValue' ts) bs
+  (vs, rest) <- S.runStateT (traverse (readFiniteValue' BigEndian) ts) bs
+  case rest of
+    [] -> return vs
+    _ -> Nothing
+
+readFiniteValuesLE :: [FiniteType] -> [Bool] -> Maybe [FiniteValue]
+readFiniteValuesLE ts bs = do
+  (vs, rest) <- S.runStateT (traverse (readFiniteValue' LittleEndian) ts) bs
   case rest of
     [] -> return vs
     _ -> Nothing
 
 readFiniteValue :: FiniteType -> [Bool] -> Maybe FiniteValue
 readFiniteValue t bs = do
-  (v, rest) <- S.runStateT (readFiniteValue' t) bs
+  (v, rest) <- S.runStateT (readFiniteValue' BigEndian t) bs
   case rest of
     [] -> return v
     _ -> Nothing

src/SAWScript/Prover/ABC.hs

@@ -29,7 +29,7 @@ import qualified Verifier.SAW.Simulator.BitBlast as BBSim
 import SAWScript.Proof(Prop, propToSATQuery, propSize, goalProp, ProofGoal, goalType, goalNum, CEX)
 import SAWScript.Prover.SolverStats (SolverStats, solverStats)
 import qualified SAWScript.Prover.Exporter as Exporter
-import SAWScript.Prover.Util (liftCexBB)
+import SAWScript.Prover.Util (liftCexBB, liftLECexBB)
 
 -- crucible-jvm
 -- TODO, very weird import
@@ -105,12 +105,11 @@ w4AbcVerilog unints sc _hashcons goal = liftIO $
        let stats = solverStats "abc_verilog" (propSize goal)
        res <- if all isSpace cexText
               then return Nothing
-                      -- NB: reverse bits to get bit-order convention right
-              else do bits <- reverse <$> parseAigerCex cexText
-                      case liftCexBB (reverse argTys) bits of
+              else do bits <- parseAigerCex cexText
+                      case liftLECexBB argTys bits of
                         Left parseErr -> fail parseErr
                         Right vs -> return $ Just model
-                          where model = zip argNames (map toFirstOrderValue (reverse vs))
+                          where model = zip argNames (map toFirstOrderValue vs)
        return (res, stats)
 
 parseAigerCex :: String -> IO [Bool]

src/SAWScript/Prover/Exporter.hs

@@ -6,6 +6,7 @@
 {-# Language ExplicitForAll #-}
 {-# Language FlexibleContexts #-}
 {-# Language TypeApplications #-}
+{-# Language TupleSections #-}
 module SAWScript.Prover.Exporter
   ( proveWithSATExporter
   , proveWithPropExporter
@@ -51,11 +52,13 @@ import qualified Data.AIG as AIG
 import qualified Data.ByteString as BS
 import Data.Parameterized.Nonce (globalNonceGenerator)
 import Data.Parameterized.Some (Some(..))
+import qualified Data.Map as Map
 import Data.Set (Set)
 import qualified Data.SBV.Dynamic as SBV
 import System.Directory (removeFile)
 import System.IO
 import System.IO.Temp(emptySystemTempFile)
+import Data.Text (pack)
 import Data.Text.Prettyprint.Doc.Render.Text
 import Prettyprinter (vcat)
 
@@ -72,7 +75,7 @@ import Verifier.SAW.Recognizer (asPi)
 import Verifier.SAW.SATQuery
 import Verifier.SAW.SharedTerm as SC
 import qualified Verifier.SAW.Translation.Coq as Coq
-import Verifier.SAW.TypedAST (mkModuleName)
+import Verifier.SAW.TypedAST (mkModuleName, toShortName)
 import Verifier.SAW.TypedTerm
 import qualified Verifier.SAW.Simulator.BitBlast as BBSim
 import qualified Verifier.SAW.Simulator.Value as Sim
@@ -90,7 +93,10 @@ import SAWScript.Prover.What4
 import SAWScript.Value
 
 import qualified What4.Expr.Builder as W4
+import What4.Config (extendConfig)
+import What4.Interface (getConfiguration)
 import What4.Protocol.SMTLib2 (writeDefaultSMT2)
+import What4.Protocol.SMTLib2.Response (smtParseOptions)
 import What4.Protocol.VerilogWriter (exprsVerilog)
 import What4.Solver.Adapter
 import qualified What4.SWord as W4Sim
@@ -275,9 +281,11 @@ writeSMTLib2 sc f satq = io $
 writeSMTLib2What4 :: SharedContext -> FilePath -> SATQuery -> TopLevel ()
 writeSMTLib2What4 sc f satq = io $
   do sym <- W4.newExprBuilder W4.FloatRealRepr St globalNonceGenerator
-     (_argNames, _argTys, _labels, lit) <- W.w4Solve sym sc satq
+     (_varMap, lit) <- W.w4Solve sym sc satq
+     let cfg = getConfiguration sym
+     extendConfig smtParseOptions cfg
      withFile f WriteMode $ \h ->
-       writeDefaultSMT2 () "Offline SMTLib2" defaultWriteSMTLIB2Features sym h [lit]
+       writeDefaultSMT2 () "Offline SMTLib2" defaultWriteSMTLIB2Features Nothing sym h [lit]
 
 writeCore :: FilePath -> Term -> TopLevel ()
 writeCore path t = io $ writeFile path (scWriteExternal t)
@@ -288,13 +296,22 @@ write_verilog sc path t = io $ writeVerilog sc path t
 writeVerilogSAT :: MonadIO m => SharedContext -> FilePath -> SATQuery -> m ([ExtCns Term],[FiniteType])
 writeVerilogSAT sc path satq = liftIO $
   do sym <- newSAWCoreBackend sc
-     (argNames, argTys, _lbls, bval) <- W.w4Solve sym sc satq
+     -- For SAT checking, we don't care what order the variables are in,
+     -- but only that we can correctly keep track of the connection
+     -- between inputs and assignments.
+     let varList  = Map.toList (satVariables satq)
+     let argNames = map fst varList
+     let argTys = map snd varList
+     (vars, bval) <- W.w4Solve sym sc satq
      let f fot = case toFiniteType fot of
                    Nothing -> fail $ "writeVerilogSAT: Unsupported argument type " ++ show fot
                    Just ft -> return ft
+     let argSValues = map (snd . snd) vars
+     let argSValueNames = zip argSValues (map (toShortName . ecName) argNames)
      argTys' <- traverse f argTys
-
-     edoc <- runExceptT $ exprsVerilog sym [Some bval] "f"
+     let mkInput (v, nm) = map (,nm) <$> flattenSValue v
+     ins <- concat <$> mapM mkInput argSValueNames
+     edoc <- runExceptT $ exprsVerilog sym ins [Some bval] "f"
      case edoc of
        Left err -> fail $ "Failed to translate to Verilog: " ++ err
        Right doc -> do
@@ -323,9 +340,15 @@ writeVerilog :: SharedContext -> FilePath -> Term -> IO ()
 writeVerilog sc path t = do
   sym <- newSAWCoreBackend sc
   st  <- sawCoreState sym
-  (_, (_, sval)) <- W4Sim.w4EvalAny sym st sc mempty mempty t
+  -- For writing Verilog in the general case, it's convenient for any
+  -- lambda-bound inputs to appear first in the module input list, in
+  -- order, followed by free variables (probably in the order seen
+  -- during traversal, because that's at least _a_ deterministic order).
+  (argNames, args, (_, sval)) <- W4Sim.w4EvalAny sym st sc mempty mempty t
   es <- flattenSValue sval
-  edoc <- runExceptT $ exprsVerilog sym es "f"
+  let mkInput (v, nm) = map (, pack nm) <$> flattenSValue v
+  ins <- concat <$> mapM mkInput (zip args argNames)
+  edoc <- runExceptT $ exprsVerilog sym ins es "f"
   case edoc of
     Left err -> fail $ "Failed to translate to Verilog: " ++ err
     Right doc -> do

src/SAWScript/Prover/Util.hs

@@ -28,3 +28,10 @@ liftCexBB tys bs =
   case readFiniteValues tys bs of
     Nothing -> Left "Failed to lift counterexample"
     Just fvs -> Right fvs
+
+-- | Lift a counterexample containing little-endian words
+liftLECexBB :: [FiniteType] -> [Bool] -> Either String [FiniteValue]
+liftLECexBB tys bs =
+  case readFiniteValuesLE tys bs of
+    Nothing -> Left "Failed to lift counterexample"
+    Just fvs -> Right fvs

src/SAWScript/Prover/What4.hs

@@ -9,9 +9,11 @@ module SAWScript.Prover.What4 where
 import System.IO
 
 import           Data.Set (Set)
+import qualified Data.Map as Map
 
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.FiniteValue
+import Verifier.SAW.SATQuery (SATQuery(..))
 
 import           SAWScript.Proof(Prop, propToSATQuery, propSize, CEX)
 import           SAWScript.Prover.SolverStats
@@ -122,7 +124,10 @@ setupWhat4_solver solver sym unintSet sc goal =
   do
      -- symbolically evaluate
      satq <- propToSATQuery sc unintSet goal
-     (argNames, _argTys, bvs, lit) <- W.w4Solve sym sc satq
+     let varList  = Map.toList (satVariables satq)
+     let argNames = map fst varList
+     (varMap, lit) <- W.w4Solve sym sc satq
+     let bvs = map (fst . snd) varMap
 
      extendConfig (solver_adapter_config_options solver)
                   (getConfiguration sym)