Merge branch 'master' into bugfix-global-infer-performance

GaloisInc · Aug 20, 2021 · 7f5bbff · 7f5bbff
2 parents 0aacaf9 + d76cdf4
commit 7f5bbff
Show file tree

Hide file tree

Showing 18 changed files with 482 additions and 306 deletions.
diff --git a/deps/aig b/deps/aig
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/cryptol b/deps/cryptol
diff --git a/deps/dwarf b/deps/dwarf
diff --git a/deps/elf-edit b/deps/elf-edit
diff --git a/deps/macaw b/deps/macaw
diff --git a/deps/what4 b/deps/what4
diff --git a/heapster-saw/examples/arrays.v b/heapster-saw/examples/arrays.v
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
@@ -3621,6 +3621,15 @@ simplify1PermForDetVars det_vars x (ValPerm_Conj ps)
     getPerm x >>>= \new_p ->
     simplify1PermForDetVars det_vars x new_p
 
+-- For lowned permission l:lowned[ls](ps_in -o ps_out), end any lifetimes in ls
+-- that are not determined and remove them from the lowned permission for ls
+simplify1PermForDetVars det_vars l (ValPerm_LOwned ls _ _)
+  | l':_ <- flip mapMaybe ls (asVar >=> \l' ->
+                               if NameSet.member l' det_vars then Nothing
+                               else return l') =
+    implEndLifetimeRecM l' >>>
+    getPerm l >>>= \p' -> simplify1PermForDetVars det_vars l p'
+
 -- If none of the above cases match but p has only determined free variables,
 -- just leave p as is
 simplify1PermForDetVars det_vars _ p

diff --git a/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v b/saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v
@@ -583,8 +583,11 @@ Definition ecRotR : forall (m : @Num), forall (ix : Type), forall (a : Type), @P
 Definition ecCat : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq m a -> @seq n a -> @seq (@tcAdd m n) a :=
   @finNumRec (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq m a -> @seq n a -> @seq (@tcAdd m n) a) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m a -> @seq n a -> @seq (@tcAdd (@TCNum m) n) a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) => @SAWCorePrelude.append m n a) (fun (a : Type) => @SAWCorePrelude.streamAppend a m)).
 
-Definition ecSplitAt : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> prod (@seq m a) (@seq n a) :=
-  @finNumRec (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> prod (@seq m a) (@seq n a)) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCNum m) n) a -> prod (@SAWCoreVectorsAsCoqVectors.Vec m a) (@seq n a)) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec (@SAWCorePrelude.addNat m n) a) => pair (@SAWCorePrelude.take a m n xs) (@SAWCorePrelude.drop a m n xs)) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => pair (@SAWCorePrelude.streamTake a m xs) (@SAWCorePrelude.streamDrop a m xs))).
+Definition ecTake : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq m a :=
+  @CryptolPrimitivesForSAWCore.Num_rect (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq m a) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCNum m) n) a -> @SAWCoreVectorsAsCoqVectors.Vec m a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec (@SAWCorePrelude.addNat m n) a) => @SAWCorePrelude.take a m n xs) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => @SAWCorePrelude.streamTake a m xs)) (@CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCInf) n) a -> @SAWCorePrelude.Stream a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCorePrelude.Stream a) => xs) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => xs)).
+
+Definition ecDrop : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq n a :=
+  @finNumRec (fun (m : @Num) => forall (n : @Num), forall (a : Type), @seq (@tcAdd m n) a -> @seq n a) (fun (m : @SAWCoreScaffolding.Nat) => @CryptolPrimitivesForSAWCore.Num_rect (fun (n : @Num) => forall (a : Type), @seq (@tcAdd (@TCNum m) n) a -> @seq n a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec (@SAWCorePrelude.addNat m n) a) => @SAWCorePrelude.drop a m n xs) (fun (a : Type) (xs : @SAWCorePrelude.Stream a) => @SAWCorePrelude.streamDrop a m xs)).
 
 Definition ecJoin : forall (m : @Num), forall (n : @Num), forall (a : Type), @seq m (@seq n a) -> @seq (@tcMul m n) a :=
   fun (m : @Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (m1 : @Num) => forall (n : @Num), forall (a : Type), @seq m1 (@seq n a) -> @seq (@tcMul m1 n) a) (fun (m1 : @SAWCoreScaffolding.Nat) => @finNumRec (fun (n : @Num) => forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec m1 (@seq n a) -> @seq (@tcMul (@TCNum m1) n) a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) => @SAWCorePrelude.join m1 n a)) (@finNumRec (fun (n : @Num) => forall (a : Type), @SAWCorePrelude.Stream (@seq n a) -> @seq (@tcMul (@TCInf) n) a) (fun (n : @SAWCoreScaffolding.Nat) (a : Type) => @SAWCorePrelude.natCase (fun (n' : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.Stream (@SAWCoreVectorsAsCoqVectors.Vec n' a) -> @seq (@SAWCorePrelude.if0Nat (@Num) n' (@TCNum 0) (@TCInf)) a) (fun (s : @SAWCorePrelude.Stream (@SAWCoreVectorsAsCoqVectors.Vec 0 a)) => @SAWCoreVectorsAsCoqVectors.EmptyVec a) (fun (n' : @SAWCoreScaffolding.Nat) (s : @SAWCorePrelude.Stream (@SAWCoreVectorsAsCoqVectors.Vec (@SAWCoreScaffolding.Succ n') a)) => @SAWCorePrelude.streamJoin a n' s) n)) m.

diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq.hs
@@ -113,7 +113,11 @@ Import ListNotations.
 translateTermAsDeclImports ::
   TranslationConfiguration -> Coq.Ident -> Term -> Either (TranslationError Term) (Doc ann)
 translateTermAsDeclImports configuration name t = do
-  doc <- TermTranslation.translateDefDoc configuration Nothing [] name t
+  doc <-
+    TermTranslation.translateDefDoc
+      configuration
+      (TermTranslation.TranslationReader Nothing)
+      [] name t
   return $ vcat [preamble configuration, hardline <> doc]
 
 translateSAWModule :: TranslationConfiguration -> Module -> Doc ann
@@ -131,7 +135,11 @@ translateSAWModule configuration m =
      ]
 
 translateCryptolModule ::
-  TranslationConfiguration -> [String] -> CryptolModule -> Either (TranslationError Term) (Doc ann)
+  TranslationConfiguration ->
+  -- | List of already translated global declarations
+  [String] ->
+  CryptolModule ->
+  Either (TranslationError Term) (Doc ann)
 translateCryptolModule configuration globalDecls m =
   let decls = CryptolModuleTranslation.translateCryptolModule
               configuration

diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/CryptolModule.hs
@@ -8,10 +8,10 @@ import           Control.Monad                      (forM)
 import           Control.Monad.State                (modify)
 import qualified Data.Map                           as Map
 
-import           Cryptol.ModuleSystem.Name
-import           Cryptol.Utils.Ident
+import           Cryptol.ModuleSystem.Name          (Name, nameIdent)
+import           Cryptol.Utils.Ident                (unpackIdent)
 import qualified Language.Coq.AST                   as Coq
-import           Verifier.SAW.Term.Functor
+import           Verifier.SAW.Term.Functor          (Term)
 import           Verifier.SAW.Translation.Coq.Monad
 import qualified Verifier.SAW.Translation.Coq.Term  as TermTranslation
 import           Verifier.SAW.TypedTerm
@@ -23,21 +23,28 @@ translateTypedTermMap tm = forM (Map.assocs tm) translateAndRegisterEntry
     translateAndRegisterEntry (name, symbol) = do
       let t = ttTerm symbol
       let nameStr = unpackIdent (nameIdent name)
-      term <- TermTranslation.withLocalLocalEnvironment $ do
+      term <- TermTranslation.withLocalTranslationState $ do
         modify $ set TermTranslation.localEnvironment [nameStr]
         TermTranslation.translateTerm t
       let decl = TermTranslation.mkDefinition nameStr term
       modify $ over TermTranslation.globalDeclarations (nameStr :)
       return decl
 
+-- | Translates a Cryptol Module into a list of Coq declarations.  This is done
+-- by going through the term map corresponding to the module, translating all
+-- terms, and accumulating the translated declarations of all top-level
+-- declarations encountered.
 translateCryptolModule ::
-  TranslationConfiguration -> [String] -> CryptolModule -> Either (TranslationError Term) [Coq.Decl]
+  TranslationConfiguration ->
+  -- | List of already translated global declarations
+  [String] ->
+  CryptolModule ->
+  Either (TranslationError Term) [Coq.Decl]
 translateCryptolModule configuration globalDecls (CryptolModule _ tm) =
-  case TermTranslation.runTermTranslationMonad
-       configuration
-       Nothing
-       globalDecls
-       []
-       (translateTypedTermMap tm) of
-  Left e -> Left e
-  Right (_, st) -> Right (reverse (view TermTranslation.localDeclarations st))
+  reverse . view TermTranslation.topLevelDeclarations . snd
+  <$> TermTranslation.runTermTranslationMonad
+      configuration
+      (TermTranslation.TranslationReader Nothing) -- TODO: this should be Just no?
+      globalDecls
+      []
+      (translateTypedTermMap tm)
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Monad.hs
@@ -17,6 +17,7 @@ module Verifier.SAW.Translation.Coq.Monad
   , TranslationConfigurationMonad
   , TranslationMonad
   , TranslationError(..)
+  , WithTranslationConfiguration(..)
   , runTranslationMonad
   ) where
 
@@ -77,19 +78,32 @@ data TranslationConfiguration = TranslationConfiguration
   -- - SAWCoreVectorsAsSSReflectSeqs
   }
 
-type TranslationConfigurationMonad m =
-  ( MonadReader TranslationConfiguration m
+-- | The functional dependency of 'MonadReader' makes it not compositional, so
+-- we have to jam together different structures that want to be in the 'Reader'
+-- into a single datatype.  This type allows adding extra configuration on top
+-- of the translation configuration.
+data WithTranslationConfiguration r = WithTranslationConfiguration
+  { translationConfiguration :: TranslationConfiguration
+  , otherConfiguration :: r
+  }
+
+-- | Some computations will rely solely on access to the configuration, so we
+-- provide it separately.
+type TranslationConfigurationMonad r m =
+  ( MonadReader (WithTranslationConfiguration r) m
   )
 
-type TranslationMonad s m =
+type TranslationMonad r s m =
   ( Except.MonadError (TranslationError Term)  m
-  , TranslationConfigurationMonad m
+  , TranslationConfigurationMonad r m
   , MonadState s m
   )
 
 runTranslationMonad ::
   TranslationConfiguration ->
+  r ->
   s ->
-  (forall m. TranslationMonad s m => m a) ->
+  (forall m. TranslationMonad r s m => m a) ->
   Either (TranslationError Term) (a, s)
-runTranslationMonad configuration state m = runStateT (runReaderT m configuration) state
+runTranslationMonad configuration r s m =
+  runStateT (runReaderT m (WithTranslationConfiguration configuration r)) s
diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs
@@ -24,10 +24,8 @@ Portability : portable
 
 module Verifier.SAW.Translation.Coq.SAWModule where
 
-import           Control.Lens                                  (makeLenses, view)
 import qualified Control.Monad.Except                          as Except
 import           Control.Monad.Reader                          hiding (fail)
-import           Control.Monad.State                           hiding (fail)
 import           Prelude                                       hiding (fail)
 import           Prettyprinter                                 (Doc)
 
@@ -36,26 +34,22 @@ import qualified Language.Coq.Pretty                           as Coq
 import           Verifier.SAW.Module
 import           Verifier.SAW.SharedTerm
 import           Verifier.SAW.Term.Functor
-import           Verifier.SAW.Translation.Coq.Monad
+import qualified Verifier.SAW.Translation.Coq.Monad            as M
 import           Verifier.SAW.Translation.Coq.SpecialTreatment
 import qualified Verifier.SAW.Translation.Coq.Term             as TermTranslation
+import Verifier.SAW.Translation.Coq.Monad
 
 -- import Debug.Trace
 
-data ModuleTranslationState = ModuleTranslationState
-  { _currentModule  :: Maybe ModuleName
-  }
-  deriving (Show)
-makeLenses ''ModuleTranslationState
-
-type ModuleTranslationMonad m = TranslationMonad ModuleTranslationState m
+type ModuleTranslationMonad m =
+  M.TranslationMonad TermTranslation.TranslationReader () m
 
 runModuleTranslationMonad ::
-  TranslationConfiguration -> Maybe ModuleName ->
+  M.TranslationConfiguration -> Maybe ModuleName ->
   (forall m. ModuleTranslationMonad m => m a) ->
-  Either (TranslationError Term) (a, ModuleTranslationState)
-runModuleTranslationMonad configuration modname =
-  runTranslationMonad configuration (ModuleTranslationState modname)
+  Either (M.TranslationError Term) (a, ())
+runModuleTranslationMonad configuration modName =
+  M.runTranslationMonad configuration (TermTranslation.TranslationReader modName) ()
 
 dropPi :: Coq.Term -> Coq.Term
 dropPi (Coq.Pi (_ : t) r) = Coq.Pi t r
@@ -162,15 +156,19 @@ liftTermTranslationMonad ::
   (forall n. TermTranslation.TermTranslationMonad   n => n a) ->
   (forall m. ModuleTranslationMonad m => m a)
 liftTermTranslationMonad n = do
-  configuration <- ask
-  cur_mod <- view currentModule <$> get
-  let r = TermTranslation.runTermTranslationMonad configuration cur_mod [] [] n
+  configuration <- asks translationConfiguration
+  configReader <- asks otherConfiguration
+  let r = TermTranslation.runTermTranslationMonad configuration configReader [] [] n
   case r of
     Left  e      -> Except.throwError e
     Right (a, _) -> do
       return a
 
-translateDecl :: TranslationConfiguration -> Maybe ModuleName -> ModuleDecl -> Doc ann
+translateDecl ::
+  M.TranslationConfiguration ->
+  Maybe ModuleName ->
+  ModuleDecl ->
+  Doc ann
 translateDecl configuration modname decl =
   case decl of
   TypeDecl td -> do

diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
@@ -25,7 +25,7 @@ Portability : portable
 module Verifier.SAW.Translation.Coq.SpecialTreatment where
 
 import           Control.Lens                       (_1, _2, over)
-import           Control.Monad.Reader               (ask)
+import           Control.Monad.Reader               (asks)
 import qualified Data.Map                           as Map
 import           Data.String.Interpolate            (i)
 import qualified Data.Text                          as Text
@@ -70,10 +70,10 @@ translateModuleName mn =
   Map.findWithDefault mn mn moduleRenamingMap
 
 findSpecialTreatment ::
-  TranslationConfigurationMonad m =>
+  TranslationConfigurationMonad r m =>
   Ident -> m IdentSpecialTreatment
 findSpecialTreatment ident = do
-  configuration <- ask
+  configuration <- asks translationConfiguration
   let moduleMap =
         Map.findWithDefault Map.empty (identModule ident) (specialTreatmentMap configuration)
   let defaultTreatment =
+5 −0		crucible-concurrency/.gitignore
+2 −1		crucible-concurrency/test/Main.hs
+1 −1		crucible-go/src/Lang/Crucible/Go/Overrides.hs
+3 −3		crucible-go/src/Lang/Crucible/Go/Simulate.hs
+2 −4		crucible-go/tool/Main.hs
+1 −0		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs
+26 −2		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs
+8 −5		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
+36 −1		crucible-llvm/test/TestMemory.hs
+4 −0		crucible/src/Lang/Crucible/Backend.hs
+26 −0		crux-llvm/crux-llvm.cabal
+94 −0		crux-llvm/for-ide/Main.hs
+34 −0		crux-llvm/for-ide/unix/RealMain.hs
+10 −0		crux-llvm/for-ide/windows/RealMain.hs
+14 −10		crux-llvm/src/Crux/LLVM/Compile.hs
+5 −0		crux-llvm/src/Crux/LLVM/Log.hs
+42 −13		crux-llvm/src/CruxLLVMMain.hs
+2 −0		crux-llvm/svcomp/Main.hs
+7 −0		crux-llvm/svcomp/SVComp/Log.hs
+6 −0		crux-llvm/test-data/golden/T784-fail.c
+4 −0		crux-llvm/test-data/golden/T784-fail.good
+6 −0		crux-llvm/test-data/golden/T784-pass.c
+1 −0		crux-llvm/test-data/golden/T784-pass.good
+5 −0		crux-llvm/test-data/golden/T787.c
+4 −0		crux-llvm/test-data/golden/T787.good
+6 −1		crux-mir/src/Mir/Language.hs
+7 −1		crux-mir/src/Mir/Log.hs
+3 −0		crux/src/Crux.hs
+26 −2		crux/src/Crux/Config.hs
+5 −1		crux/src/Crux/SVCOMP.hs
+6 −35		uc-crux-llvm/src/UCCrux/LLVM/Config.hs
+5 −0		uc-crux-llvm/src/UCCrux/LLVM/Logging.hs
+6 −1		uc-crux-llvm/src/UCCrux/LLVM/Main.hs
+6 −0		uc-crux-llvm/test/Test.hs
+2 −0		uc-crux-llvm/uc-crux-llvm.cabal
+12 −13		.github/workflows/ci.yml
+6 −0		CHANGES.md
+5 −0		cryptol-remote-api/python/CHANGELOG.md
+29 −16		cryptol-remote-api/python/cryptol/connection.py
+25 −22		cryptol-remote-api/python/poetry.lock
+2 −2		cryptol-remote-api/python/pyproject.toml
+41 −9		cryptol-remote-api/python/tests/cryptol/test_basics.py
+1 −0		cryptol-remote-api/run_rpc_tests.sh
+13 −2		cryptol-remote-api/src/CryptolServer.hs
+4 −2		cryptol-remote-api/src/CryptolServer/LoadModule.hs
+1 −1		cryptol.cabal
+1 −1		deps/argo
+17 −10		src/Cryptol/Eval/SBV.hs
+10 −7		src/Cryptol/Eval/What4.hs
+3 −1		src/Cryptol/ModuleSystem.hs
+7 −7		src/Cryptol/ModuleSystem/Base.hs
+23 −18		src/Cryptol/ModuleSystem/Env.hs
+17 −18		src/Cryptol/ModuleSystem/Exports.hs
+5 −1		src/Cryptol/ModuleSystem/Renamer.hs
+42 −3		src/Cryptol/Parser.y
+1 −1		src/Cryptol/Parser/AST.hs
+10 −9		src/Cryptol/REPL/Command.hs
+2 −1		src/Cryptol/TypeCheck.hs
+1 −1		src/Cryptol/TypeCheck/Infer.hs
+2 −3		src/Cryptol/TypeCheck/Monad.hs
+17 −8		src/Cryptol/TypeCheck/Solver/SMT.hs
+8 −0		src/Cryptol/TypeCheck/Subst.hs
+0 −2		tests/regression/ignore-safe.icry
+0 −2		tests/regression/ignore-safe.icry.stdout
+42 −0		tests/regression/repl-decls.icry
+27 −0		tests/regression/repl-decls.icry.stdout
+337 −303		src/Data/Dwarf.hs
+180 −179		src/Data/Dwarf/CFA.hs
+126 −94		src/Data/Dwarf/Types.hs
+3 −3		src/Data/ElfEdit.hs
+1 −1		src/Data/ElfEdit/HighLevel/Layout.hs
+3 −2		src/Data/ElfEdit/Prim/Ehdr.hs
+5 −5		src/Data/ElfEdit/Prim/SymbolTable.hs
+7 −1		.github/workflows/test.yml
+8 −5		what4/src/What4/Expr/VarIdentification.hs
+17 −0		what4/src/What4/ProblemFeatures.hs
+24 −5		what4/src/What4/Protocol/SMTWriter.hs
+6 −2		what4/src/What4/Solver/CVC4.hs
+18 −0		what4/test/ExprBuilderSMTLib2.hs
+0 −1		what4/what4.cabal