Refactored saw-core-coq (#1928)

* Changed the type-checker to *not* normalize argument types in lambdas and pis when they are type-checked, in order to make the Coq translation work in cases where these argument types have identifiers that translate to alternate Coq definitions

* added the termIsClosed function to test if a SAW core term is closed

* refactored the saw-core-coq translator so that all the local variable information is in a reader effect and not a state effect, making it clearer where in the translator code variables are bound; also fixed #1927

* replaced llvmZeroInitValue with a new function translateZeroInit that directly translates an LLVM zero initializer to a Heapster permission + SAW core term, so that we use repeatBVVec in the SAW term rather than a giant vector literal

* updated mbox_proofs.v after changes to the Coq translator

* renamed askTrr and localTrr to askTR and localTR

* replaced a number of equality tests on the free variables of terms against emptyBitSet with the new termIsClosed function

* replaced checkGroundTerm with the now standard termIsClosed function

* whoops, fixed a few lingering bugs related to using termIsClosed

* made a few fixes to make the code more readable

* a few more tweaks to make the code look nicer

* finished writing a comment on withSAWVar

* indentation change requested by review

heapster-saw/examples/mbox_proofs.v

@@ -64,7 +64,7 @@ Proof.
             (bvSub 64 i strt)
             len
             (bvSub 64 bv64_128 strt)
-            e
+            _1
             pf1)) as H.
     rewrite bvAdd_Sub_cancel. intros H.
     rewrite (UIP_bool _ _ H pf).

heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs

@@ -54,6 +54,14 @@ bvVecValueOpenTerm w tp ts def_tm =
    def_tm, natOpenTerm (natValue w),
    bvLitOfIntOpenTerm (intValue w) (fromIntegral $ length ts)]
 
+-- | Helper function to build a SAW core term of type @BVVec w len a@, i.e., a
+-- bitvector-indexed vector, containing a single repeated value
+repeatBVVecOpenTerm :: NatRepr w -> OpenTerm -> OpenTerm -> OpenTerm ->
+                       OpenTerm
+repeatBVVecOpenTerm w len tp t =
+  applyOpenTermMulti (globalOpenTerm "Prelude.repeatBVVec")
+  [natOpenTerm (natValue w), len, tp, t]
+
 -- | The information needed to translate an LLVM global to Heapster
 data LLVMTransInfo = LLVMTransInfo {
   llvmTransInfoEnv :: PermEnv,
@@ -111,8 +119,7 @@ translateLLVMValue w _ (L.ValArray tp elems) =
 
     -- Generate a default element of type tp using the zero initializer; this is
     -- currently needed by bvVecValueOpenTerm
-    def_v <- llvmZeroInitValue tp
-    (_,def_tm) <- translateLLVMValue w tp def_v
+    (_,def_tm) <- translateZeroInit w tp
 
     -- Finally, build our array shape and SAW core value
     return (PExpr_ArrayShape (bvInt $ fromIntegral $ length elems) sh_len sh,
@@ -150,7 +157,7 @@ translateLLVMValue w tp (L.ValString bytes) =
 translateLLVMValue w _ (L.ValConstExpr ce) =
   translateLLVMConstExpr w ce
 translateLLVMValue w tp L.ValZeroInit =
-  llvmZeroInitValue tp >>= translateLLVMValue w tp
+  translateZeroInit w tp
 translateLLVMValue _ _ v =
   traceAndZeroM ("translateLLVMValue does not yet handle:\n" ++ ppLLVMValue v)
 
@@ -218,14 +225,30 @@ translateLLVMGEP _ tp vtrans ixs
     isZeroIdx _                = False
 
 -- | Build an LLVM value for a @zeroinitializer@ field of the supplied type
-llvmZeroInitValue :: L.Type -> LLVMTransM (L.Value)
-llvmZeroInitValue (L.PrimType (L.Integer _)) = return $ L.ValInteger 0
-llvmZeroInitValue (L.Array len tp) =
-  L.ValArray tp <$> replicate (fromIntegral len) <$> llvmZeroInitValue tp
-llvmZeroInitValue (L.PackedStruct tps) =
-  L.ValPackedStruct <$> zipWith L.Typed tps <$> mapM llvmZeroInitValue tps
-llvmZeroInitValue tp =
-  traceAndZeroM ("llvmZeroInitValue cannot handle type:\n"
+translateZeroInit :: (1 <= w, KnownNat w) => NatRepr w -> L.Type ->
+                     LLVMTransM (PermExpr (LLVMShapeType w), OpenTerm)
+translateZeroInit w tp@(L.PrimType (L.Integer _)) =
+   translateLLVMValue w tp (L.ValInteger 0)
+translateZeroInit w (L.Array len tp) =
+  -- First, translate the zero element and its type
+  do (sh, elem_tm) <- translateZeroInit w tp
+     (_, saw_tp) <- translateLLVMType w tp
+
+     -- Compute the array stride as the length of the element shape
+     sh_len_expr <- lift $ llvmShapeLength sh
+     sh_len <- fromInteger <$> lift (bvMatchConstInt sh_len_expr)
+
+     let arr_len = bvInt $ fromIntegral len
+     let saw_len = bvLitOfIntOpenTerm (intValue w) (fromIntegral len)
+     return (PExpr_ArrayShape arr_len sh_len sh,
+             repeatBVVecOpenTerm w saw_len saw_tp elem_tm)
+
+translateZeroInit w (L.PackedStruct tps) =
+  mapM (translateZeroInit w) tps >>= \(unzip -> (shs,ts)) ->
+  return (foldr PExpr_SeqShape PExpr_EmptyShape shs, tupleOpenTerm ts)
+
+translateZeroInit _ tp =
+  traceAndZeroM ("translateZeroInit cannot handle type:\n"
                  ++ show (L.ppType tp))
 
 -- | Top-level call to 'translateLLVMValue', running the 'LLVMTransM' monad

saw-core-coq/src/Verifier/SAW/Translation/Coq.hs

@@ -121,7 +121,7 @@ translateTermAsDeclImports configuration name t tp = do
   doc <-
     TermTranslation.translateDefDoc
       configuration
-      (TermTranslation.TranslationReader Nothing)
+      Nothing
       [] name t tp
   return $ vcat [preamble configuration, hardline <> doc]
 

saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs

@@ -3,7 +3,7 @@
 
 module Verifier.SAW.Translation.Coq.CryptolModule where
 
-import           Control.Lens                       (over, set, view)
+import           Control.Lens                       (over, view)
 import           Control.Monad                      (forM)
 import           Control.Monad.State                (modify)
 import qualified Data.Map                           as Map
@@ -27,9 +27,7 @@ translateTypedTermMap defs = forM defs translateAndRegisterEntry
     translateAndRegisterEntry (name, t, tp) = do
       let nameStr = unpackIdent (nameIdent name)
       decl <-
-        TermTranslation.withLocalTranslationState $
-        do modify $ set TermTranslation.localEnvironment [nameStr]
-           t_trans <- TermTranslation.translateTerm t
+        do t_trans <- TermTranslation.translateTerm t
            tp_trans <- TermTranslation.translateTerm tp
            return $ TermTranslation.mkDefinition nameStr t_trans tp_trans
       modify $ over TermTranslation.globalDeclarations (nameStr :)
@@ -55,7 +53,7 @@ translateCryptolModule sc env configuration globalDecls (CryptolModule _ tm) =
        (reverse . view TermTranslation.topLevelDeclarations . snd <$>
         TermTranslation.runTermTranslationMonad
         configuration
-        (TermTranslation.TranslationReader Nothing) -- TODO: this should be Just no?
+        Nothing -- TODO: this should be Just no?
         globalDecls
         []
         (translateTypedTermMap defs))

saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs

@@ -42,14 +42,14 @@ import Verifier.SAW.Translation.Coq.Monad
 -- import Debug.Trace
 
 type ModuleTranslationMonad m =
-  M.TranslationMonad TermTranslation.TranslationReader () m
+  M.TranslationMonad (Maybe ModuleName) () m
 
 runModuleTranslationMonad ::
   M.TranslationConfiguration -> Maybe ModuleName ->
   (forall m. ModuleTranslationMonad m => m a) ->
   Either (M.TranslationError Term) (a, ())
 runModuleTranslationMonad configuration modName =
-  M.runTranslationMonad configuration (TermTranslation.TranslationReader modName) ()
+  M.runTranslationMonad configuration modName ()
 
 dropPi :: Coq.Term -> Coq.Term
 dropPi (Coq.Pi (_ : t) r) = Coq.Pi t r
@@ -93,22 +93,22 @@ translateDataType (DataType {..}) =
     translateNamed name = do
       let inductiveName = name
       (inductiveParameters, inductiveIndices) <-
-        liftTermTranslationMonad $ do
-        ps <- TermTranslation.translateParams dtParams
-        ixs <- TermTranslation.translateParams dtIndices
+        liftTermTranslationMonad $
+        TermTranslation.translateParams dtParams $ \ps ->
+        TermTranslation.translateParams dtIndices $ \ixs ->
         -- Translating the indices of a data type should never yield
         -- Inhabited constraints, so the result of calling
         -- `translateParams dtIndices` above should only return Binders and not
         -- any ImplicitBinders. Moreover, `translateParams` always returns
         -- Binders where the second field is `Just t`, where `t` is the type.
-        let errorBecause msg = error $ "translateDataType.translateNamed: " ++ msg
+        let errorBecause msg = error $ "translateDataType.translateNamed: " ++ msg in
         let bs = map (\case Coq.Binder s (Just t) ->
                               Coq.PiBinder (Just s) t
                             Coq.Binder _ Nothing ->
                               errorBecause "encountered a Binder without a Type"
                             Coq.ImplicitBinder{} ->
                               errorBecause "encountered an implicit binder")
-                     ixs
+                     ixs in
         return (ps, bs)
       let inductiveSort = TermTranslation.translateSort dtSort
       inductiveConstructors <- mapM (translateCtor inductiveParameters) dtCtors