Merge pull request #1863 from GaloisInc/T1859-mir_load_module

Implement `mir_load_module`

CHANGES.md

@@ -95,6 +95,10 @@
   on Windows at this time due to a downstream issue with CVC5 1.0.4 and
   earlier.)
 
+* Add experimental support for verifying Rust programs. For more information,
+  see the `mir_*` commands documented in the
+  [SAW manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md).
+
 # Version 0.9
 
 ## New Features

README.md

@@ -6,7 +6,8 @@ This repository contains the code for SAWScript, the scripting
 language that forms the primary user interface to the Software
 Analysis Workbench (SAW). It provides the ability to reason about
 formal models describing the denotation of programs written in
-languages such as C, Java, and Cryptol.
+languages such as C, Java, and Cryptol. It also provides experimental,
+incomplete support for the Rust language.
 
 ## Documentation
 

doc/manual/manual.md

@@ -5,7 +5,8 @@ mathematical models of the computational behavior of software,
 transforming these models, and proving properties about them.
 
 SAW can currently construct models of a subset of programs written in
-Cryptol, LLVM (and therefore C), and JVM (and therefore Java). The
+Cryptol, LLVM (and therefore C), and JVM (and therefore Java). SAW also has
+experimental, incomplete support for MIR (and therefore Rust). The
 models take the form of typed functional programs, so in a sense SAW can
 be considered a translator from imperative programs to their functional
 equivalents. Various external proof tools, including a variety of SAT
@@ -176,7 +177,7 @@ Cryptol, Haskell and ML. In particular, functions are applied by
 writing them next to their arguments rather than by using parentheses
 and commas. Rather than writing `f(x, y)`, write `f x y`.
 
-Comments are written as in C and Java (among many other languages). All
+Comments are written as in C, Java, and Rust (among many other languages). All
 text from `//` until the end of a line is ignored. Additionally, all
 text between `/*` and `*/` is ignored, regardless of whether the line
 ends.
@@ -1568,6 +1569,8 @@ analyze JVM and LLVM programs.
 
 The first step in analyzing any code is to load it into the system.
 
+## Loading LLVM
+
 To load LLVM code, simply provide the location of a valid bitcode file
 to the `llvm_load_module` function.
 
@@ -1583,6 +1586,8 @@ most likely case of incompleteness. We aim to support every version
 after 3.5, however, so report any parsing failures as [on
 GitHub](https://github.com/GaloisInc/saw-script/issues).
 
+## Loading Java
+
 Loading Java code is slightly more complex, because of the more
 structured nature of Java packages. First, when running `saw`, three flags
 control where to look for classes:
@@ -1623,12 +1628,28 @@ unresolved issues in verifying code involving classes such as `String`. For
 more information on these issues, refer to
 [this GitHub issue](https://github.com/GaloisInc/crucible/issues/641).
 
+## Loading MIR
+
+To load a piece of Rust code, first compile it to a MIR JSON file, as described
+in [this section](#compiling-mir), and then provide the location of the JSON
+file to the `mir_load_module` function:
+
+* `mir_load_module : String -> TopLevel MIRModule`
+
+SAW currently supports Rust code that can be built with a [March 22, 2020 Rust
+nightly](https://static.rust-lang.org/dist/2020-03-22/).  If you encounter a
+Rust feature that SAW does not support, please report it [on
+GitHub](https://github.com/GaloisInc/saw-script/issues).
+
 ## Notes on Compiling Code for SAW
 
-SAW will generally be able to load arbitrary LLVM bitcode and JVM
-bytecode files, but several guidelines can help make verification
-easier or more likely to succeed. For generating LLVM with `clang`, it
-can be helpful to:
+SAW will generally be able to load arbitrary LLVM bitcode, JVM bytecode, and
+MIR JSON files, but several guidelines can help make verification easier or
+more likely to succeed.
+
+### Compiling LLVM
+
+For generating LLVM with `clang`, it can be helpful to:
 
 * Turn on debugging symbols with `-g` so that SAW can find source
   locations of functions, names of variables, etc.
@@ -1659,11 +1680,54 @@ behavior, and SAW currently does not have built in support for these
 functions (though you could manually create overrides for them in a
 verification script).
 
+[^1]: https://clang.llvm.org/docs/UsersManual.html#controlling-code-generation
+
+### Compiling Java
+
 For Java, the only compilation flag that tends to be valuable is `-g` to
 retain information about the names of function arguments and local
 variables.
 
-[^1]: https://clang.llvm.org/docs/UsersManual.html#controlling-code-generation
+### Compiling MIR
+
+In order to verify Rust code, SAW analyzes Rust's MIR (mid-level intermediate
+representation) language. In particular, SAW analyzes a particular form of MIR
+that the [`mir-json`](https://github.com/GaloisInc/mir-json) tool produces. You
+will need to intall `mir-json` and run it on Rust code in order to produce MIR
+JSON files that SAW can load (see [this section](#loading-mir)).
+
+For `cargo`-based projects, `mir-json` provides a `cargo` subcommand called
+`cargo saw-build` that builds a JSON file suitable for use with SAW. `cargo
+saw-build` integrates directly with `cargo`, so you can pass flags to it like
+any other `cargo` subcommand. For example:
+
+```
+$ export SAW_RUST_LIBRARY_PATH=<...>
+$ cargo saw-build <other cargo flags>
+<snip>
+linking 11 mir files into <...>/example-364cf2df365c7055.linked-mir.json
+<snip>
+```
+
+Note that:
+
+* The full output of `cargo saw-build` here is omitted. The important part is
+  the `.linked-mir.json` file that appears after `linking X mir files into`, as
+  that is the JSON file that must be loaded with SAW.
+* `SAW_RUST_LIBRARY_PATH` should point to the the MIR JSON files for the Rust
+  standard library.
+
+`mir-json` also supports compiling individual `.rs` files through `mir-json`'s
+`saw-rustc` command. As the name suggests, it accepts all of the flags that
+`rustc` accepts. For example:
+
+```
+$ export SAW_RUST_LIBRARY_PATH=<...>
+$ saw-rustc example.rs <other rustc flags>
+<snip>
+linking 11 mir files into <...>/example.linked-mir.json
+<snip>
+```
 
 ## Notes on C++ Analysis
 

intTests/test_mir_load_module/Makefile

@@ -0,0 +1,8 @@
+all: test.json
+
+test.linked-mir.json: test.rs
+	saw-rustc $<
+
+.PHONY: clean
+clean:
+	rm -f test.linked-mir.json

intTests/test_mir_load_module/test.linked-mir.json

@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i32"}},"pos":"test.rs:1:23: 1:25","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"int","size":4,"val":"42"},"ty":"ty::i32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:1:27: 1:27"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i32"}]},"name":"test/3a1fbbbh::foo[0]","return_ty":"ty::i32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/3a1fbbbh::foo[0]","kind":"Item","substs":[]},"name":"test/3a1fbbbh::foo[0]"}],"tys":[{"name":"ty::i32","ty":{"intkind":{"kind":"I32"},"kind":"Int"}}],"roots":["test/3a1fbbbh::foo[0]"]}

intTests/test_mir_load_module/test.rs

@@ -0,0 +1 @@
+pub fn foo() -> i32 { 42 }

intTests/test_mir_load_module/test.saw

@@ -0,0 +1,4 @@
+enable_experimental;
+
+m <- mir_load_module "test.linked-mir.json";
+print m;

intTests/test_mir_load_module/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

saw-remote-api/docs/SAW.rst

@@ -419,6 +419,32 @@ No return fields
 
 
 
+SAW/MIR/load module (command)
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Load the specified MIR module.
+
+Parameter fields
+++++++++++++++++
+
+
+``name``
+  The name to refer to the loaded module by later.
+
+
+
+``module name``
+  The file containing the MIR JSON file to load.
+
+
+
+Return fields
++++++++++++++
+
+No return fields
+
+
+
 SAW/Yosys/import (command)
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 

saw-remote-api/saw-remote-api.cabal

@@ -45,6 +45,7 @@ common deps
                  cryptol-saw-core,
                  crucible,
                  crucible-jvm,
+                 crucible-mir,
                  cryptonite,
                  cryptonite-conduit,
                  directory,
@@ -81,6 +82,7 @@ library
                    SAWServer.JVMVerify,
                    SAWServer.LLVMCrucibleSetup,
                    SAWServer.LLVMVerify,
+                   SAWServer.MIRCrucibleSetup,
                    SAWServer.NoParams,
                    SAWServer.OK,
                    SAWServer.ProofScript,

saw-remote-api/saw-remote-api/Main.hs

@@ -36,6 +36,8 @@ import SAWServer.LLVMVerify
       llvmAssume,
       llvmVerifyX86Descr,
       llvmVerifyX86 )
+import SAWServer.MIRCrucibleSetup
+    ( mirLoadModuleDescr, mirLoadModule )
 import SAWServer.ProofScript
     ( makeSimpsetDescr, makeSimpset, proveDescr, prove )
 import SAWServer.SaveTerm ( saveTermDescr, saveTerm )
@@ -114,6 +116,11 @@ sawMethods =
      "SAW/LLVM/assume"
      llvmAssumeDescr
      llvmAssume
+  -- MIR
+  , Argo.command
+      "SAW/MIR/load module"
+      mirLoadModuleDescr
+      mirLoadModule
   -- Yosys
   , Argo.command
      "SAW/Yosys/import"

saw-remote-api/src/SAWServer.hs

@@ -38,6 +38,7 @@ import qualified Data.AIG as AIG
 import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator, newHandleAllocator)
 import qualified Lang.Crucible.JVM as CJ
 import qualified Lang.JVM.Codebase as JSS
+import Mir.Generator (RustModule)
 --import qualified Verifier.SAW.CryptolEnv as CryptolEnv
 import Verifier.SAW.Module (emptyModule)
 import Verifier.SAW.SharedTerm (mkSharedContext, scLoadModule)
@@ -78,7 +79,8 @@ import SAWServer.Exceptions
       notAJVMClass,
       notAJVMMethodSpecIR,
       notAYosysImport,
-      notAYosysTheorem, notAYosysSequential
+      notAYosysTheorem, notAYosysSequential,
+      notAMIRModule
     )
 
 type SAWCont = (SAWEnv, SAWTask)
@@ -317,12 +319,13 @@ data ServerVal
   | VJVMCrucibleSetup (Pair CrucibleSetupTypeRepr JVMSetupM)
   | VLLVMCrucibleSetup (Pair CrucibleSetupTypeRepr LLVMCrucibleSetupM)
   | VLLVMModule (Some CMS.LLVMModule)
+  | VMIRModule RustModule
   | VJVMMethodSpecIR (CMS.ProvedSpec CJ.JVM)
   | VLLVMMethodSpecIR (CMS.SomeLLVM CMS.ProvedSpec)
   | VGhostVar CMS.GhostGlobal
   | VYosysImport YosysImport
   | VYosysTheorem YosysTheorem
-  | VYosysSequential YosysSequential 
+  | VYosysSequential YosysSequential
 
 instance Show ServerVal where
   show (VTerm t) = "(VTerm " ++ show t ++ ")"
@@ -333,6 +336,7 @@ instance Show ServerVal where
   show (VJVMCrucibleSetup _) = "VJVMCrucibleSetup"
   show (VLLVMCrucibleSetup _) = "VLLVMCrucibleSetup"
   show (VLLVMModule (Some _)) = "VLLVMModule"
+  show (VMIRModule _) = "VMIRModule"
   show (VLLVMMethodSpecIR _) = "VLLVMMethodSpecIR"
   show (VJVMMethodSpecIR _) = "VJVMMethodSpecIR"
   show (VGhostVar x) = "(VGhostVar " ++ show x ++ ")"
@@ -391,6 +395,9 @@ instance KnownCrucibleSetupType a => IsServerVal (LLVMCrucibleSetupM a) where
 instance IsServerVal (Some CMS.LLVMModule) where
   toServerVal = VLLVMModule
 
+instance IsServerVal RustModule where
+  toServerVal = VMIRModule
+
 setServerVal :: IsServerVal val => ServerName -> val -> Argo.Command SAWState ()
 setServerVal name val =
   do Argo.debugLog $ "Saving " <> (T.pack (show name))
@@ -438,6 +445,13 @@ getLLVMModule n =
        VLLVMModule m -> return m
        _other -> Argo.raise (notAnLLVMModule n)
 
+getMIRModule :: ServerName -> Argo.Command SAWState RustModule
+getMIRModule n =
+  do v <- getServerVal n
+     case v of
+       VMIRModule m -> return m
+       _other -> Argo.raise (notAMIRModule n)
+
 getLLVMSetup :: ServerName -> Argo.Command SAWState (Pair CrucibleSetupTypeRepr LLVMCrucibleSetupM)
 getLLVMSetup n =
   do v <- getServerVal n

saw-remote-api/src/SAWServer/Exceptions.hs

@@ -14,6 +14,7 @@ module SAWServer.Exceptions (
   , notAYosysTheorem
   , notAYosysImport
   , notAYosysSequential
+  , notAMIRModule
   -- * Wrong monad errors
   , notSettingUpCryptol
   , notSettingUpLLVMCrucible
@@ -192,6 +193,17 @@ notAYosysSequential name =
      " is not a Yosys sequential module")
     (Just $ object ["name" .= name])
 
+notAMIRModule ::
+  (ToJSON name, Show name) =>
+  name {- ^ the name that should have been mapped to a MIR module -}->
+  JSONRPCException
+notAMIRModule name =
+  makeJSONRPCException 10140
+    ("The server value with name " <>
+     T.pack (show name) <>
+     " is not a MIR module")
+    (Just $ object ["name" .= name])
+
 cantLoadLLVMModule :: String -> JSONRPCException
 cantLoadLLVMModule err =
   makeJSONRPCException

saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs

@@ -0,0 +1,57 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
+-- | Support for interfacing with MIR-related commands in SAW.
+module SAWServer.MIRCrucibleSetup
+  ( mirLoadModule
+  , mirLoadModuleDescr
+  ) where
+
+import Control.Lens ( view )
+import Data.Aeson ( FromJSON(..), withObject, (.:) )
+
+import SAWScript.Crucible.MIR.Builtins ( mir_load_module )
+
+import qualified Argo
+import qualified Argo.Doc as Doc
+import SAWServer as Server
+    ( ServerName(..),
+      SAWState,
+      sawTask,
+      setServerVal )
+import SAWServer.Exceptions ( notAtTopLevel )
+import SAWServer.OK ( OK, ok )
+import SAWServer.TopLevel ( tl )
+import SAWServer.TrackFile ( trackFile )
+
+data MIRLoadModuleParams
+  = MIRLoadModuleParams ServerName FilePath
+
+instance FromJSON MIRLoadModuleParams where
+  parseJSON =
+    withObject "params for \"SAW/MIR/load module\"" $ \o ->
+    MIRLoadModuleParams <$> o .: "name" <*> o .: "module name"
+
+instance Doc.DescribedMethod MIRLoadModuleParams OK where
+  parameterFieldDescription =
+    [ ("name",
+        Doc.Paragraph [Doc.Text "The name to refer to the loaded module by later."])
+    , ("module name",
+       Doc.Paragraph [Doc.Text "The file containing the MIR JSON file to load."])
+    ]
+  resultFieldDescription = []
+
+mirLoadModuleDescr :: Doc.Block
+mirLoadModuleDescr =
+  Doc.Paragraph [Doc.Text "Load the specified MIR module."]
+
+-- | The implementation of the @SAW/MIR/load module@ command.
+mirLoadModule :: MIRLoadModuleParams -> Argo.Command SAWState OK
+mirLoadModule (MIRLoadModuleParams serverName fileName) =
+  do tasks <- view sawTask <$> Argo.getState
+     case tasks of
+       (_:_) -> Argo.raise $ notAtTopLevel $ map fst tasks
+       [] ->
+         do mirMod <- tl $ mir_load_module fileName
+            setServerVal serverName mirMod
+            trackFile fileName
+            ok