Add preliminary support for model checker query

.gitmodules

@@ -43,3 +43,6 @@
 [submodule "deps/language-rust"]
 	path = deps/language-rust
 	url = https://github.com/harpocrates/language-rust.git
+[submodule "deps/language-sally"]
+	path = deps/language-sally
+	url = https://github.com/GaloisInc/language-sally

cabal.project

@@ -17,6 +17,8 @@ packages:
     deps/aig
     deps/cryptol
     deps/what4/what4
+    deps/what4/what4-transition-system
+    deps/language-sally
     deps/crucible/crucible
     deps/crucible/crucible-concurrency
     deps/crucible/crucible-jvm

saw-script.cabal

@@ -83,6 +83,8 @@ library
     , unordered-containers
     , utf8-string
     , what4 >= 0.4
+    , what4-transition-system
+    , language-sally
     , vector
     , GraphSCC
     , macaw-base
@@ -180,6 +182,7 @@ library
     SAWScript.Yosys.Netgraph
     SAWScript.Yosys.State
     SAWScript.Yosys.Theorem
+    SAWScript.Yosys.TransitionSystem
     SAWScript.Yosys.Utils
 
   GHC-options: -O2 -Wall -fno-ignore-asserts -fno-spec-constr-count

src/SAWScript/Interpreter.hs

@@ -3359,6 +3359,11 @@ primitives = Map.fromList
     Experimental
     []
 
+  , prim "yosys_verify_sequential_offline_sally"  "YosysSequential -> String -> Term -> TopLevel ()"
+    (pureVal yosys_verify_sequential_sally)
+    Experimental
+    []
+
     ---------------------------------------------------------------------
 
   , prim "mr_solver_prove" "Term -> Term -> TopLevel ()"

src/SAWScript/Yosys.hs

@@ -14,6 +14,7 @@ module SAWScript.Yosys
   , yosys_import_sequential
   , yosys_extract_sequential
   , yosys_extract_sequential_raw
+  , yosys_verify_sequential_sally
   , loadYosysIR
   , yosysIRToTypedTerms
   ) where
@@ -22,14 +23,13 @@ import Control.Lens.TH (makeLenses)
 
 import Control.Lens (view, (^.))
 import Control.Exception (throw)
-import Control.Monad (forM, foldM)
+import Control.Monad (foldM)
 import Control.Monad.IO.Class (MonadIO(..))
 
 import qualified Data.List.NonEmpty as NE
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Text (Text)
-import qualified Data.Text as Text
 import qualified Data.Graph as Graph
 
 import qualified Text.URI as URI
@@ -43,12 +43,14 @@ import qualified Cryptol.Utils.RecordMap as C
 
 import SAWScript.Value
 import qualified SAWScript.Builtins as Builtins
+import qualified SAWScript.Crucible.Common as Common
 
 import SAWScript.Yosys.Utils
 import SAWScript.Yosys.IR
 import SAWScript.Yosys.Netgraph
 import SAWScript.Yosys.State
 import SAWScript.Yosys.Theorem
+import SAWScript.Yosys.TransitionSystem
 
 --------------------------------------------------------------------------------
 -- ** Building the module graph from Yosys IR
@@ -182,3 +184,10 @@ yosys_extract_sequential s n = do
 
 yosys_extract_sequential_raw :: YosysSequential -> TopLevel SC.TypedTerm
 yosys_extract_sequential_raw s = pure $ s ^. yosysSequentialTerm
+
+yosys_verify_sequential_sally :: YosysSequential -> FilePath -> SC.TypedTerm -> TopLevel ()
+yosys_verify_sequential_sally s path q = do
+  sc <- getSharedContext
+  sym <- liftIO $ Common.newSAWCoreExprBuilder sc
+  scs <- liftIO $ Common.sawCoreState sym
+  queryModelChecker sym scs sc s path q

src/SAWScript/Yosys/State.hs

@@ -53,6 +53,8 @@ data YosysSequential = YosysSequential
   , _yosysSequentialStateFields :: Map Text (SC.Term, C.Type)
   , _yosysSequentialInputFields :: Map Text (SC.Term, C.Type)
   , _yosysSequentialOutputFields :: Map Text (SC.Term, C.Type)
+  , _yosysSequentialInputWidths :: Map Text Natural
+  , _yosysSequentialOutputWidths :: Map Text Natural
   , _yosysSequentialStateWidths :: Map Text Natural
   }
 makeLenses ''YosysSequential
@@ -171,6 +173,8 @@ convertModuleInline sc m = do
     , _yosysSequentialStateFields = stateFields
     , _yosysSequentialInputFields = inputFields
     , _yosysSequentialOutputFields = outputFields
+    , _yosysSequentialInputWidths = fromIntegral . length <$> inputPorts
+    , _yosysSequentialOutputWidths = fromIntegral . length <$> outputPorts
     , _yosysSequentialStateWidths = stateWidths
     }