From ff072a87475779951445808f70036defa3ca917c Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 16 Mar 2022 10:16:33 -0700
Subject: [PATCH] Adapt saw-script to changed tuple representation.

---
 src/SAWScript/Crucible/Common/MethodSpec.hs   |  2 +-
 src/SAWScript/Crucible/LLVM/Builtins.hs       |  4 +--
 .../Crucible/LLVM/ResolveSetupValue.hs        |  5 ++--
 src/SAWScript/Crucible/LLVM/X86.hs            |  4 +--
 src/SAWScript/Prover/Exporter.hs              |  9 ++----
 src/SAWScript/Prover/MRSolver/Monad.hs        |  7 ++---
 src/SAWScript/Prover/MRSolver/SMT.hs          | 30 ++++++++++---------
 src/SAWScript/Prover/MRSolver/Solver.hs       |  9 +-----
 src/SAWScript/Prover/MRSolver/Term.hs         | 16 ++++------
 src/SAWScript/SBVParser.hs                    |  2 +-
 10 files changed, 37 insertions(+), 51 deletions(-)

diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs
index 5d9249a824..2cf69b8cef 100644
--- a/src/SAWScript/Crucible/Common/MethodSpec.hs
+++ b/src/SAWScript/Crucible/Common/MethodSpec.hs
@@ -255,7 +255,7 @@ setupToTerm opts sc =
 
         SetupStruct _ _ fs ->
           do st <- setupToTerm opts sc base
-             lift $ scTupleSelector sc st ind (length fs)
+             lift $ scTupleSelector sc st ind
 
         _ -> MaybeT $ return Nothing
 
diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index ba1ad5e1a1..3d9777a9c9 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -414,9 +414,9 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic =
           input_terms <- io $ traverse (scExtCns shared_context) input_parameters
           applied_extracted_func <- io $ scApplyAll shared_context extracted_func_const input_terms
           applied_extracted_func_selectors <-
-            io $ forM [1 .. (length output_parameters)] $ \i ->
+            io $ forM [0 .. (length output_parameters - 1)] $ \i ->
             mkTypedTerm shared_context
-              =<< scTupleSelector shared_context applied_extracted_func i (length output_parameters)
+              =<< scTupleSelector shared_context applied_extracted_func i
           let output_parameter_substitution =
                 Map.fromList $
                 zip (map ecVarIndex output_parameters) (map ttTerm applied_extracted_func_selectors)
diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
index fb37eae978..b5374b1829 100644
--- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -838,7 +838,7 @@ resolveSAWTerm cc tp tm =
       Cryptol.TVTuple tps ->
         do st <- sawCoreState sym
            let sc = saw_ctx st
-           tms <- mapM (\i -> scTupleSelector sc tm i (length tps)) [1 .. length tps]
+           tms <- mapM (scTupleSelector sc tm) [0 .. length tps - 1]
            vals <- zipWithM (resolveSAWTerm cc) tps tms
            storTy <-
              case toLLVMType dl tp of
@@ -1062,8 +1062,7 @@ memArrayToSawCoreTerm crucible_context endianess typed_term = do
               inner_saw_term <- liftIO $ scTupleSelector
                 saw_context
                 saw_term
-                (field_index + 1)
-                (length tuple_element_cryptol_types)
+                field_index
               setBytes
                 tuple_element_cryptol_type
                 inner_saw_term
diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs
index e95786b426..958cb3d84f 100644
--- a/src/SAWScript/Crucible/LLVM/X86.hs
+++ b/src/SAWScript/Crucible/LLVM/X86.hs
@@ -566,8 +566,8 @@ setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func =
        arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) ->
          toSC sym sawst $ Crucible.LLVM.Fixpoint.headerValue fixpoint_entry
        applied_func <- scApplyAll sc (ttTerm func) $ implicit_parameters ++ arguments
-       applied_func_selectors <- forM [1 .. (length fixpoint_substitution_as_list)] $ \i ->
-         scTupleSelector sc applied_func i (length fixpoint_substitution_as_list)
+       applied_func_selectors <- forM [0 .. (length fixpoint_substitution_as_list - 1)] $ \i ->
+         scTupleSelector sc applied_func i
        result_substitution <- MapF.fromList <$> zipWithM
          (\(MapF.Pair variable _) applied_func_selector ->
            MapF.Pair variable <$> bindSAWTerm sym sawst (W4.exprType variable) applied_func_selector)
diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs
index 63d66a18bf..9e48e4ea3c 100644
--- a/src/SAWScript/Prover/Exporter.hs
+++ b/src/SAWScript/Prover/Exporter.hs
@@ -343,12 +343,9 @@ writeVerilogSAT path satq = getSharedContext >>= \sc -> io $
 flattenSValue :: IsSymExprBuilder sym => sym -> W4Sim.SValue sym -> IO [Some (W4.SymExpr sym)]
 flattenSValue _ (Sim.VBool b) = return [Some b]
 flattenSValue _ (Sim.VWord (W4Sim.DBV w)) = return [Some w]
-flattenSValue sym (Sim.VPair l r) =
-  do lv <- Sim.force l
-     rv <- Sim.force r
-     ls <- flattenSValue sym lv
-     rs <- flattenSValue sym rv
-     return (ls ++ rs)
+flattenSValue sym (Sim.VTuple ts) =
+  do vs <- traverse Sim.force ts
+     concat <$> traverse (flattenSValue sym) vs
 flattenSValue sym (Sim.VVector ts) =
   do vs <- mapM Sim.force ts
      let getBool (Sim.VBool b) = Just b
diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs
index 71e79735ba..d2eb06be5c 100644
--- a/src/SAWScript/Prover/MRSolver/Monad.hs
+++ b/src/SAWScript/Prover/MRSolver/Monad.hs
@@ -438,15 +438,14 @@ liftSC5 f a b c d e = mrSC >>= \sc -> liftIO (f sc a b c d e)
 
 -- | Apply a 'TermProj' to perform a projection on a 'Term'
 doTermProj :: Term -> TermProj -> MRM Term
-doTermProj t TermProjLeft = liftSC1 scPairLeft t
-doTermProj t TermProjRight = liftSC1 scPairRight t
+doTermProj t (TermProjTuple i) = liftSC1 (\sc x -> scTupleSelector sc x i) t
 doTermProj t (TermProjRecord fld) = liftSC2 scRecordSelect t fld
 
 -- | Apply a 'TermProj' to a type to get the output type of the projection,
 -- assuming that the type is already normalized
 doTypeProj :: Term -> TermProj -> MRM Term
-doTypeProj (asPairType -> Just (tp1, _)) TermProjLeft = return tp1
-doTypeProj (asPairType -> Just (_, tp2)) TermProjRight = return tp2
+doTypeProj (asTupleType -> Just tps) (TermProjTuple i)
+  | i < length tps = pure (tps !! i)
 doTypeProj (asRecordType -> Just tp_map) (TermProjRecord fld)
   | Just tp <- Map.lookup fld tp_map
   = return tp
diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs
index efb196f0bc..406a69d4fe 100644
--- a/src/SAWScript/Prover/MRSolver/SMT.hs
+++ b/src/SAWScript/Prover/MRSolver/SMT.hs
@@ -221,11 +221,9 @@ mrProvable bool_tm =
                (closedOpenTerm a)
              ec <- instUVar nm ec_tp
              liftSC4 genBVVecTerm n len a ec
-          -- For pairs, recurse on both sides and combine the result as a pair
-          (asPairType -> Just (tp1, tp2)) -> do
-            e1 <- instUVar nm tp1
-            e2 <- instUVar nm tp2
-            liftSC2 scPairValue e1 e2
+          -- For tuples, recurse on all components and combine the result as a tuple
+          (asTupleType -> Just tps) ->
+            liftSC1 scTuple =<< traverse (instUVar nm) tps
           -- Otherwise, create a global variable with the given name and type
           tp' -> liftSC2 scFreshEC nm tp' >>= liftSC1 scExtCns
 
@@ -268,6 +266,12 @@ andTermInCtx (TermInCtx ctx1 t1) (TermInCtx ctx2 t2) =
     t2' <- liftTermLike (length ctx2) (length ctx1) t2
     TermInCtx (ctx1++ctx2) <$> liftSC2 scAnd t1' t2'
 
+-- | Conjoin a list of 'TermInCtx's, assuming they all have Boolean type.
+allTermInCtx :: [TermInCtx] -> MRM TermInCtx
+allTermInCtx [] = TermInCtx [] <$> liftSC1 scBool True
+allTermInCtx [x] = pure x
+allTermInCtx (x : xs) = andTermInCtx x =<< allTermInCtx xs
+
 -- | Extend the context of a 'TermInCtx' with additional universal variables
 -- bound "outside" the 'TermInCtx'
 extTermInCtx :: [(LocalName,Term)] -> TermInCtx -> TermInCtx
@@ -358,15 +362,13 @@ mrProveEqH _ (asBoolType -> Just _) t1 t2 =
 mrProveEqH _ (asIntegerType -> Just _) t1 t2 =
   mrProveEqSimple (liftSC2 scIntEq) t1 t2
 
--- For pair types, prove both the left and right projections are equal
-mrProveEqH var_map (asPairType -> Just (tpL, tpR)) t1 t2 =
-  do t1L <- liftSC1 scPairLeft t1
-     t2L <- liftSC1 scPairLeft t2
-     t1R <- liftSC1 scPairRight t1
-     t2R <- liftSC1 scPairRight t2
-     condL <- mrProveEqH var_map tpL t1L t2L
-     condR <- mrProveEqH var_map tpR t1R t2R
-     andTermInCtx condL condR
+-- For tuple types, prove all of the projections are equal
+mrProveEqH var_map (asTupleType -> Just tps) t1 t2 =
+  do let idxs = [0 .. length tps - 1]
+     ts1 <- liftSC1 (\sc t -> traverse (scTupleSelector sc t) idxs) t1
+     ts2 <- liftSC1 (\sc t -> traverse (scTupleSelector sc t) idxs) t2
+     conds <- sequence $ zipWith3 (mrProveEqH var_map) tps ts1 ts2
+     allTermInCtx conds
 
 -- For non-bitvector vector types, prove all projections are equal by
 -- quantifying over a universal index variable and proving equality at that
diff --git a/src/SAWScript/Prover/MRSolver/Solver.hs b/src/SAWScript/Prover/MRSolver/Solver.hs
index f6b711a1e7..278d9e12f8 100644
--- a/src/SAWScript/Prover/MRSolver/Solver.hs
+++ b/src/SAWScript/Prover/MRSolver/Solver.hs
@@ -145,13 +145,6 @@ asLRTList (asCtor -> Just (primName -> "Prelude.LRT_Cons", [lrt, lrts])) =
      (tp_norm_closed :) <$> asLRTList lrts
 asLRTList t = throwMRFailure (MalformedLetRecTypes t)
 
--- | Match a right-nested series of pairs. This is similar to 'asTupleValue'
--- except that it expects a unit value to always be at the end.
-asNestedPairs :: Recognizer Term [Term]
-asNestedPairs (asPairValue -> Just (x, asNestedPairs -> Just xs)) = Just (x:xs)
-asNestedPairs (asFTermF -> Just UnitValue) = Just []
-asNestedPairs _ = Nothing
-
 -- | Bind fresh function variables for a @letRecM@ or @multiFixM@ with the given
 -- @LetRecTypes@ and definitions for the function bodies as a lambda
 mrFreshLetRecVars :: Term -> Term -> MRM [Term]
@@ -169,7 +162,7 @@ mrFreshLetRecVars lrts defs_f =
     -- the definitions of the individual letrec-bound functions in terms of the
     -- new function constants
     defs_tm <- mrApplyAll defs_f fun_tms
-    defs <- case asNestedPairs defs_tm of
+    defs <- case asTupleValue defs_tm of
       Just defs -> return defs
       Nothing -> throwMRFailure (MalformedDefsFun defs_f)
 
diff --git a/src/SAWScript/Prover/MRSolver/Term.hs b/src/SAWScript/Prover/MRSolver/Term.hs
index cd7a10c86d..8b27a85a72 100644
--- a/src/SAWScript/Prover/MRSolver/Term.hs
+++ b/src/SAWScript/Prover/MRSolver/Term.hs
@@ -64,16 +64,15 @@ showMRVar :: MRVar -> String
 showMRVar = show . ppName . ecName . unMRVar
 
 -- | A tuple or record projection of a 'Term'
-data TermProj = TermProjLeft | TermProjRight | TermProjRecord FieldName
+data TermProj = TermProjTuple Int | TermProjRecord FieldName
               deriving (Eq, Ord, Show)
 
 -- | Recognize a 'Term' as 0 or more projections
 asProjAll :: Term -> (Term, [TermProj])
 asProjAll (asRecordSelector -> Just ((asProjAll -> (t, projs)), fld)) =
   (t, TermProjRecord fld:projs)
-asProjAll (asPairSelector -> Just ((asProjAll -> (t, projs)), isRight))
-  | isRight = (t, TermProjRight:projs)
-  | not isRight = (t, TermProjLeft:projs)
+asProjAll (asTupleSelector -> Just ((asProjAll -> (t, projs)), i)) =
+  (t, TermProjTuple i : projs)
 asProjAll t = (t, [])
 
 -- | Names of functions to be used in computations, which are either names bound
@@ -100,10 +99,8 @@ funNameTerm :: FunName -> Term
 funNameTerm (LetRecName var) = Unshared $ FTermF $ ExtCns $ unMRVar var
 funNameTerm (EVarFunName var) = Unshared $ FTermF $ ExtCns $ unMRVar var
 funNameTerm (GlobalName gdef []) = globalDefTerm gdef
-funNameTerm (GlobalName gdef (TermProjLeft:projs)) =
-  Unshared $ FTermF $ PairLeft $ funNameTerm (GlobalName gdef projs)
-funNameTerm (GlobalName gdef (TermProjRight:projs)) =
-  Unshared $ FTermF $ PairRight $ funNameTerm (GlobalName gdef projs)
+funNameTerm (GlobalName gdef (TermProjTuple i : projs)) =
+  Unshared $ FTermF $ TupleSelector (funNameTerm (GlobalName gdef projs)) i
 funNameTerm (GlobalName gdef (TermProjRecord fname:projs)) =
   Unshared $ FTermF $ RecordProj (funNameTerm (GlobalName gdef projs)) fname
 
@@ -381,8 +378,7 @@ instance PrettyInCtx [Term] where
   prettyInCtx xs = list <$> mapM prettyInCtx xs
 
 instance PrettyInCtx TermProj where
-  prettyInCtx TermProjLeft = return (pretty '.' <> "1")
-  prettyInCtx TermProjRight = return (pretty '.' <> "2")
+  prettyInCtx (TermProjTuple i) = return (pretty '.' <> pretty i)
   prettyInCtx (TermProjRecord fld) = return (pretty '.' <> pretty fld)
 
 instance PrettyInCtx FunName where
diff --git a/src/SAWScript/SBVParser.hs b/src/SAWScript/SBVParser.hs
index 8f16083c79..dfcf4d49f4 100644
--- a/src/SAWScript/SBVParser.hs
+++ b/src/SAWScript/SBVParser.hs
@@ -263,7 +263,7 @@ scTyp sc (TRecord fields) =
 splitInputs :: SharedContext -> Typ -> Term -> IO [Term]
 splitInputs _sc TBool x = return [x]
 splitInputs sc (TTuple ts) x =
-    do xs <- mapM (\i -> scTupleSelector sc x i (length ts)) [1 .. length ts]
+    do xs <- mapM (scTupleSelector sc x) [0 .. length ts - 1]
        yss <- sequence (zipWith (splitInputs sc) ts xs)
        return (concat yss)
 splitInputs _ (TVec _ TBool) x = return [x]