crux-mir-comp: allow references in imported cryptol

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

@@ -343,6 +343,10 @@ regToTermWithAdapt sym sc name w4VarMapRef ada0 shp0 rv0 = go ada0 shp0 rv0
             terms <- goVector a shp' vec
             tyTerm <- shapeToTerm' sc a shp'
             liftIO $ SAW.scVector sc tyTerm terms
+        (AdaptDerefRef col elAda, RefShape _ty elT M.Immut tpr, mirPtr) ->
+             do r <- readMirRefSim tpr mirPtr
+                let elShp = tyToShapeEq col elT tpr
+                go elAda elShp r
         (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 ->

crux-mir-comp/DESIGN.md

@@ -201,6 +201,7 @@ rules:
     of basic Rust numeric types (e.g., `usize`)
   * Symbolic expressions may *not* be used as arguments corresponding to
     numeric type parameters.
+  * References in function arguments are transparently dereferenced.
   * 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`

crux-mir-comp/src/Mir/Cryptol.hs

@@ -590,6 +590,10 @@ typecheckFnSig col fnSig argShps0 (Some retShp) (SAW.TypedTermSchema sch@(Cry.Fo
            | not isArg -> typeErr desc shp ty "Slice references may appear only in parameters"
            | Just (len,cryEl) <- Cry.tIsSeq ty ->
              AdaptDerefSlice col len <$> goOne isArg desc (tyToShapeEq col elTy elTyRepr) cryEl
+        (RefShape _refTy elTy M.Immut elTyRepr, _)
+           | not isArg -> typeErr desc shp ty "References may appear only in parameters"
+           | otherwise ->
+             AdaptDerefRef col <$> goOne isArg desc (tyToShapeEq col elTy elTyRepr) ty
 
         _ -> typeErr desc shp ty ""
 

saw-central/src/SAWCentral/Crucible/MIR/TypeShape.hs

@@ -398,6 +398,7 @@ data CryTermAdaptor a =
     -- We also store the 'M.Collection' here so that we can convert the
     -- element type's 'TypeRepr' to a 'TypeShape' when we need to (see,
     -- for instance, the implementation of `shapeToTerm'`).
+  | AdaptDerefRef M.Collection (CryTermAdaptor a) -- ^ Transparently adapt a reference
     deriving (Functor, Foldable, Traversable)
 
 isCryNoAdapt :: CryTermAdaptor a -> Bool
@@ -456,6 +457,8 @@ shapeToTerm' sc = go
     go (AdaptDerefSlice col n ada) (SliceShape _ elT M.Immut tpr) =
       do et <- go ada (tyToShapeEq col elT tpr)
          liftIO (mkVec n et)
+    go (AdaptDerefRef col ada) (RefShape _ elT M.Immut tpr) =
+      go ada (tyToShapeEq col elT tpr)
     go _ada shp = fail $ "shapeToTerm: unsupported type " ++ show (shapeType shp)
 
     mkVec :: Integral a => a -> SAW.Term -> IO SAW.Term