Merge pull request #2670 from GaloisInc/issue_2657

Add support for using size polymorphic Cryptol functions in crux-mir-comp

Author: yav

crucible-mir-comp/src/Mir/Compositional/Convert.hs

@@ -30,6 +30,7 @@ import qualified Data.Set as Set
 import Data.Vector (Vector)
 import qualified Data.Vector as V
 import GHC.Stack (HasCallStack)
+import qualified Data.BitVector.Sized as BV
 
 import Lang.Crucible.Backend
 import Lang.Crucible.Simulator.RegValue
@@ -52,6 +53,7 @@ import SAWCentral.Crucible.MIR.TypeShape
 import Mir.Intrinsics
 import qualified Mir.Mir as M
 import Mir.Compositional.State
+import Lang.Crucible.Simulator
 
 
 -- | Run `f` on each `SymExpr` in `v`.
@@ -306,6 +308,85 @@ exprToTerm sym sc w4VarMapRef val = liftIO $ do
     term <- SAW.scVariable sc ec
     return term
 
+
+-- | Try to convert a Crucible register value into a SAW core `Term`, using
+-- a `CryTermAdaptor` to validate and convert references to slices.
+-- We check that references to slices match the expected length specified
+-- in the `CryTermAdaptor`, and if so we read out the value stored in
+-- in the slice.
+regToTermWithAdapt :: forall m p sym t fs tp0 rtp args ret.
+    ( IsSymInterface sym,
+      sym ~ MirSym t fs,
+      m ~ OverrideSim (p sym) sym MIR rtp args ret) =>
+    sym ->
+    SAW.SharedContext ->
+    String ->
+    IORef (Map SAW.VarIndex (Some (W4.Expr t))) ->
+    CryTermAdaptor Integer ->
+    TypeShape tp0 ->
+    RegValue sym tp0 ->
+    m SAW.Term
+regToTermWithAdapt sym sc name w4VarMapRef ada0 shp0 rv0 = go ada0 shp0 rv0
+  where
+    go :: forall tp.
+        CryTermAdaptor Integer ->
+        TypeShape tp ->
+        RegValue sym tp ->
+        m SAW.Term
+    go ada shp rv =
+      case (ada, shp, rv) of
+        (NoAdapt, _, _) -> regToTerm sym sc name w4VarMapRef shp rv
+        (AdaptTuple as, TupleShape _ elems, ag) -> do
+            terms <- accessMirAggregate' sym elems as ag $ \_off _sz shp' rv' a -> go a shp' rv'
+            liftIO $ SAW.scTuple sc terms
+        (AdaptArray a, ArrayShape _ _ shp', vec) -> do
+            terms <- goVector a shp' vec
+            tyTerm <- shapeToTerm' sc a shp'
+            liftIO $ SAW.scVector sc tyTerm terms
+        (AdaptDerefSlice col n elAda, SliceShape _ty elT M.Immut tpr, Ctx.Empty Ctx.:> RV mirPtr Ctx.:> RV lenExpr) ->
+          case BV.asUnsigned <$> W4.asBV lenExpr of
+            Nothing ->
+              fail "Slice length is not statically known"
+
+            Just n1
+              | n /= n1 ->
+                fail (unlines [
+                  "Slice length mismatch:",
+                  "  Expected: " ++ show n,
+                  "  Actual  : " ++ show n1
+                ])
+              | otherwise ->
+                do
+                  let elShp = tyToShapeEq col elT tpr
+                  vals <-
+                    forM [ 0 .. n - 1 ] $ \i ->
+                      do
+                        iExpr   <- liftIO (W4.bvLit sym knownNat (BV.mkBV knownNat i))
+                        elemPtr <- mirRef_offsetWrapSim mirPtr iExpr
+                        r       <- readMirRefSim tpr elemPtr
+                        go elAda elShp r
+                  elTyTerm <- shapeToTerm' sc elAda elShp
+                  liftIO (SAW.scVector sc elTyTerm vals)
+
+            
+                
+        _ -> fail $
+            "type error: " ++ name ++ " got argument of unsupported type " ++ show (shapeType shp)
+
+    goVector :: forall tp.
+        CryTermAdaptor Integer ->
+        TypeShape tp ->
+        MirVector sym tp ->
+        m [SAW.Term]
+    goVector ada shp (MirVector_Vector v) = mapM (go ada shp) $ toList v
+    goVector ada shp (MirVector_PartialVector pv) = do
+        forM (toList pv) $ \rv -> do
+            let rv' = readMaybeType sym "field" (shapeType shp) rv
+            go ada shp rv'
+    goVector _ada _shp (MirVector_Array _) = fail $
+        "regToTerm: MirVector_Array not supported"
+
+
 regToTerm :: forall sym t fs tp0 m.
     (IsSymInterface sym, sym ~ MirSym t fs, MonadIO m, MonadFail m) =>
     sym ->

crux-mir-comp/DESIGN.md

@@ -147,6 +147,74 @@ implementations of some cryptographic algorithms) are usually declared as
 immutable and thus always retain their initial values.
 
 
+## Cryptol
+
+It is possible to import Cryptol expressions into symbolic Rust test cases to
+help write specifications (e.g., if you want to check that a Rust implementation
+matches a Cryptol specification).  This is done by using the `cryptol!` macro
+defined in the `crucible` crate.  Here's an example illustrating how to
+import a Cryptol function `myCryFun` defined in Cryptol module `SomeCryMod`,
+and bind it as the Rust function `myRustFun`:
+
+```Cryptol
+module SomeCryMod where
+  f: [8] -> [32]
+  f x = 0 # x
+```
+```Rust
+use crucible::*;
+cryptol! {
+    path "SomeCryMod";
+    pub fn myRustFun(x: u8) -> u32 = r"myCryFun";
+}
+```
+
+Тhe `path` component of the macro specifies a Cryptol module,
+the string after the `=` is a Cryptol expression, and the rest of the
+declaration specifies how to invoke evaluating the Cryptol expression from
+Rust.  If the declaration contains `const` generics, then the Cryptol expression
+is specified as a format string which may refer to the values of the const
+generic parameters in curly braces (literal curly braces need to be escaped
+as a double curly brace).  Here's an example of how to use a function with
+const generics:
+```Cryptol``
+module Cryptol where
+  sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a
+  sum = foldl (+) zero
+```
+```Rust
+extern crate crucible;
+use crucible::*;
+cryptol! {
+    path "Cryptol";
+    pub fn f<const N: usize>(x: &[u8]) -> u8 = r"sum`{{{N},[8]}}";
+}
+```
+
+It is important that the type of the Cryptol expression is compatible
+with the type of the declared Rust function, according to the following
+rules:
+
+  * The Cryptol type may have only numeric type parameters
+  * The first parameters of the Rust function should correspond to the
+    numeric type parameters of the Cryptol expression; they should be
+    of basic Rust numeric types (e.g., `usize`)
+  * Symbolic expressions may *not* be used as arguments corresponding to
+    numeric type parameters.
+  * The remaining parameters to the Rust function should correspond to the
+    parameters in the Cryptol type as follows:
+      * Cryptol's `Bit` is represented as Rust's `bool`
+      * A Cryptol sequence of length `n` may be represented as a Rust
+        array of length `n`.
+      * In the parameters of the Rust function, Cryptol sequences may also
+        be represented as reference to slices.  The length of the slice should
+        match the length of the Cryptol sequence, which is checked dynamically.
+      * Cryptol `Bit` sequences of lengths corresponding to Rust's basic
+        numeric types may also be represented with those types
+        (e.g., `[8]` may be represented with `u8` or `i8`).
+      * Cryptol tuples are represented as Rust tuples.
+
+
 ## Current limitations
 
 * Only one specification can be provided at a time for each function.  There is

crux-mir-comp/crux-mir-comp.cabal

@@ -40,6 +40,9 @@ library
     parameterized-utils >= 1.0.8,
     what4,
 
+    -- galois packages from hackage
+    bv-sized,
+
     -- internal subpackages/sublibraries in the saw tree
     crucible-mir-comp,
     saw:saw-core,