WIP mir-json

- updated libs
- changed crux_mir to crux::mir in tests
- new lib build script (build.sh)
- changes to crux-mir to support changes to rustc (nightly-2023-01-22)

crucible-mir/src/Mir/GenericOps.hs

@@ -72,19 +72,21 @@ adtIndices (Adt _aname _kind vars _ _ _ _) col = go 0 vars
  lastExplicit' = if isExplicit v then discr else lastExplicit
  in discr : go lastExplicit' vs
 
- getDiscr _ (Variant name (Explicit did) _fields _knd) = case Map.lookup did (_functions col) of
+ getDiscr _ (Variant _ _ _ _ (Just i)) = i
+
+ getDiscr _ (Variant name (Explicit did) _fields _knd _) = case Map.lookup did (_functions col) of
  Just fn -> case fn^.fbody.mblocks of
- [ BasicBlock _info (BasicBlockData [Assign _lhs (Use (OpConstant (Constant _ty (ConstInt i)))) _loc] _term) ] ->
+ ( BasicBlock _info (BasicBlockData [Assign _lhs (Use (OpConstant (Constant _ty (ConstInt i)))) _loc] _term) ):_ ->
  fromIntegerLit i
 
- _ -> error "enum discriminant constant should only have one basic block"
+ _ -> error ("enum discriminant constant should only have one basic block [variant id:" ++ show _aname ++ " discr index:" ++ show name ++ "]")
 
  Nothing -> error $ "cannot find discriminant constant " ++ show did ++
  " for variant " ++ show name
- getDiscr lastExplicit (Variant _vname (Relative i) _fields _kind) =
+ getDiscr lastExplicit (Variant _vname (Relative i) _fields _kind _) =
  lastExplicit + toInteger i
 
- isExplicit (Variant _ (Explicit _) _ _) = True
+ isExplicit (Variant _ (Explicit _) _ _ _) = True
  isExplicit _ = False
 
 --------------------------------------------------------------------------------------
@@ -155,6 +157,7 @@ instance GenericOps Intrinsic
 instance GenericOps Instance
 instance GenericOps InstanceKind
 instance GenericOps NamedTy
+instance GenericOps NonDivergingIntrinsic
 
 -- instances for newtypes
 -- we need the deriving strategy 'anyclass' to disambiguate 

crucible-mir/src/Mir/JSON.hs

@@ -166,10 +166,15 @@ instance FromJSON CtorKind where
  parseJSON = withObject "CtorKind" $ \v -> case lookupKM "kind" v of
  Just (String "Fn") -> pure FnKind
  Just (String "Const") -> pure ConstKind
- Just (String "Fictive") -> pure FictiveKind
  _ -> fail "unspported constructor kind"
 instance FromJSON Variant where
- parseJSON = withObject "Variant" $ \v -> Variant <$> v .: "name" <*> v .: "discr" <*> v .: "fields" <*> v .: "ctor_kind"
+ parseJSON = withObject "Variant" $ \v ->
+ Variant <$> v .: "name"
+ <*> v .: "discr"
+ <*> v .: "fields"
+ <*> v .: "ctor_kind"
+ <*> do val <- v .:? "discr_value"
+ convertIntegerText `traverse` val
 
 instance FromJSON Field where
  parseJSON = withObject "Field" $ \v -> Field <$> v .: "name" <*> v .: "ty"
@@ -251,6 +256,19 @@ instance FromJSON Statement where
  Just (String "StorageLive") -> StorageLive <$> v .: "slvar"
  Just (String "StorageDead") -> StorageDead <$> v .: "sdvar"
  Just (String "Nop") -> pure Nop
+ Just (String "Deinit") -> pure Deinit
+ Just (String "Intrinsic") -> do
+ kind <- v .: "intrinsic_kind"
+ ndi <- case kind of
+ "Assume" -> NDIAssume <$> v .: "operand"
+ "CopyNonOverlapping" ->
+ NDICopyNonOverlapping <$> v .: "src"
+ <*> v .: "dst"
+ <*> v .: "count"
+ _ -> fail $ "unknown Intrinsic kind" ++ kind
+
+ return $ StmtIntrinsic ndi
+
  k -> fail $ "kind not found for statement: " ++ show k
 
 
@@ -290,6 +308,8 @@ instance FromJSON Rvalue where
  Just (String "UnaryOp") -> UnaryOp <$> v .: "uop" <*> v .: "op"
  Just (String "Discriminant") -> Discriminant <$> v .: "val"
  Just (String "Aggregate") -> Aggregate <$> v .: "akind" <*> v .: "ops"
+ Just (String "ShallowInitBox") -> ShallowInitBox <$> v .: "ptr" <*> v .: "ty"
+ Just (String "CopyForDeref") -> CopyForDeref <$> v .: "place"
  k -> fail $ "unsupported RValue " ++ show k
 
 instance FromJSON Terminator where
@@ -322,7 +342,7 @@ instance FromJSON Operand where
 instance FromJSON NullOp where
  parseJSON = withObject "NullOp" $ \v -> case lookupKM "kind" v of
  Just (String "SizeOf") -> pure SizeOf
- Just (String "Box") -> pure Box
+ Just (String "AlignOf") -> pure AlignOf
  x -> fail ("bad nullOp: " ++ show x)
 
 instance FromJSON BorrowKind where
@@ -374,13 +394,23 @@ instance FromJSON Vtable where
 
 instance FromJSON CastKind where
  parseJSON = withObject "CastKind" $ \v -> case lookupKM "kind" v of
- Just (String "Misc") -> pure Misc
  Just (String "Pointer(ReifyFnPointer)") -> pure ReifyFnPointer
  Just (String "Pointer(ClosureFnPointer(Normal))") -> pure ClosureFnPointer
  Just (String "Pointer(UnsafeFnPointer)") -> pure UnsafeFnPointer
  Just (String "Pointer(Unsize)") -> pure Unsize
  Just (String "Pointer(MutToConstPointer)") -> pure MutToConstPointer
  Just (String "UnsizeVtable") -> UnsizeVtable <$> v .: "vtable"
+ -- TODO: actually plumb this information through if it is relevant
+ -- instead of using Misc
+ Just (String "PointerExposeAddress") -> pure Misc
+ Just (String "PointerFromExposedAddress") -> pure Misc
+ Just (String "DynStar") -> pure Misc
+ Just (String "IntToInt") -> pure Misc
+ Just (String "FloatToInt") -> pure Misc
+ Just (String "FloatToFloat") -> pure Misc
+ Just (String "IntToFloat") -> pure Misc
+ Just (String "PtrToPtr") -> pure Misc
+ Just (String "FnPtrToPtr") -> pure Misc
  x -> fail ("bad CastKind: " ++ show x)
 
 instance FromJSON Constant where
@@ -489,6 +519,17 @@ instance FromJSON RustcRenderedConst where
  val <- convertIntegerText =<< v .: "val"
  return $ ConstRawPtr val
 
+ Just (String "array") -> do
+ elems <- map (\(RustcRenderedConst val) -> val) <$> v .: "elements"
+ return $ ConstArray elems
+
+ Just (String "tuple") -> do
+ elems <- map (\(RustcRenderedConst val) -> val) <$> v .: "elements"
+ return $ ConstArray elems
+
+ o -> do
+ fail $ "parseJSON - bad rendered constant kind: " ++ show o
+
 -- mir-json integers are expressed as strings of 128-bit unsigned values
 -- for example, -1 is displayed as "18446744073709551615"
 -- we need to parse this as a 128 unsigned bit Int value and then

crucible-mir/src/Mir/Mir.hs

@@ -196,11 +196,10 @@ data VariantDiscr
 data CtorKind
  = FnKind
  | ConstKind
- | FictiveKind
  deriving (Eq, Ord, Show, Generic)
 
 
-data Variant = Variant {_vname :: DefId, _vdiscr :: VariantDiscr, _vfields :: [Field], _vctorkind :: CtorKind}
+data Variant = Variant {_vname :: DefId, _vdiscr :: VariantDiscr, _vfields :: [Field], _vctorkind :: Maybe CtorKind, _discrval :: Maybe Integer }
  deriving (Eq, Ord,Show, Generic)
 
 
@@ -284,6 +283,13 @@ data Statement =
  | StorageLive { _slv :: Var }
  | StorageDead { _sdv :: Var }
  | Nop
+ | Deinit
+ | StmtIntrinsic NonDivergingIntrinsic
+ deriving (Show,Eq, Ord, Generic)
+
+data NonDivergingIntrinsic =
+ NDIAssume Operand
+ | NDICopyNonOverlapping Operand Operand Operand
  deriving (Show,Eq, Ord, Generic)
 
 data PlaceElem =
@@ -321,6 +327,8 @@ data Rvalue =
  | Discriminant { _dvar :: Lvalue }
  | Aggregate { _ak :: AggregateKind, _ops :: [Operand] }
  | RAdtAg AdtAg
+ | ShallowInitBox { _sibptr :: Operand, _sibty :: Ty }
+ | CopyForDeref Lvalue
  deriving (Show,Eq, Ord, Generic)
 
 data AdtAg = AdtAg { _agadt :: Adt, _avgariant :: Integer, _aops :: [Operand], _adtagty :: Ty }
@@ -377,7 +385,7 @@ data Operand =
 
 data NullOp =
  SizeOf
- | Box
+ | AlignOf
  deriving (Show,Eq, Ord, Generic)
 
 
@@ -427,15 +435,16 @@ data Vtable = Vtable
  }
  deriving (Show, Eq, Ord, Generic)
 
+-- TODO: add other castkinds (see json)
 data CastKind =
-  Misc
-  | ReifyFnPointer
-  | ClosureFnPointer
-  | UnsafeFnPointer
-  | Unsize
-  | UnsizeVtable VtableName
-  | MutToConstPointer
-  deriving (Show,Eq, Ord, Generic)
+ Misc
+ | ReifyFnPointer
+ | ClosureFnPointer
+ | UnsafeFnPointer
+ | Unsize
+ | UnsizeVtable VtableName
+ | MutToConstPointer
+ deriving (Show,Eq, Ord, Generic)
 
 data Constant = Constant Ty ConstVal
  deriving (Eq, Ord, Show, Generic)
@@ -672,7 +681,7 @@ instance TypeOf Rvalue where
  in TyTuple [resTy, TyBool]
  typeOf (NullaryOp op ty) = case op of
  SizeOf -> TyUint USize
- Box -> TyAdt (textId "type::adt") (textId "alloc::boxed::Box") (Substs [ty])
+ AlignOf -> TyUint USize
  typeOf (UnaryOp op x) =
  let ty = typeOf x
  in case op of
@@ -683,6 +692,8 @@ instance TypeOf Rvalue where
  typeOf (Aggregate AKTuple ops) = TyTuple $ map typeOf ops
  typeOf (Aggregate AKClosure ops) = TyClosure $ map typeOf ops
  typeOf (RAdtAg (AdtAg _ _ _ ty)) = ty
+ typeOf (ShallowInitBox _ ty) = ty
+ typeOf (CopyForDeref lv) = typeOf lv
 
 instance TypeOf Operand where
  typeOf (Move lv) = typeOf lv

crucible-mir/src/Mir/PP.hs

@@ -108,7 +108,9 @@ instance Pretty CtorKind where
  pretty = viaShow
 
 instance Pretty Variant where
- pretty (Variant nm dscr flds knd) = pretty_fn4 "Variant" nm dscr flds knd
+ pretty (Variant nm dscr flds knd mbVal) =
+ pretty "Variant" <>
+ tupled [pretty nm, pretty dscr, pretty flds, pretty knd, pretty mbVal]
 
 instance Pretty Field where
  pretty (Field nm ty) = pretty_fn2 "Field" nm ty
@@ -164,6 +166,13 @@ instance Pretty Statement where
  pretty (StorageLive l) = pretty_fn1 "StorageLive" l <> semi
  pretty (StorageDead l) = pretty_fn1 "StorageDead" l <> semi
  pretty Nop = pretty "nop" <> semi
+ pretty Deinit = pretty "DeInit"
+ pretty (StmtIntrinsic (NDIAssume op)) =
+ pretty "Intrinsic" <> brackets (pretty "Assume") <> parens (pretty op) <> semi
+ pretty (StmtIntrinsic (NDICopyNonOverlapping o1 o2 o3)) =
+ pretty "Intrinsic" <> brackets (pretty "CopyNonOverlapping")
+ <> tupled (pretty <$> [o1, o2, o3])
+ <> semi
 
 instance Pretty Lvalue where
  pretty (LBase base) = pretty base
@@ -196,6 +205,8 @@ instance Pretty Rvalue where
  pretty (Discriminant a) = pretty_fn1 "Discriminant" a
  pretty (Aggregate a b) = pretty_fn2 "Aggregate" a b
  pretty (RAdtAg a) = pretty a
+ pretty (ShallowInitBox ptr ty) = pretty_fn2 "ShallowInitBox" ptr ty
+ pretty (CopyForDeref lv) = pretty_fn1 "CopyForDeref" lv
 
 instance Pretty AdtAg where
  pretty (AdtAg (Adt nm _kind _vs _ _ _ _) i ops _) = pretty_fn3 "AdtAg" nm i ops
@@ -241,7 +252,7 @@ instance Pretty Constant where
 
 instance Pretty NullOp where
  pretty SizeOf = pretty "sizeof"
- pretty Box = pretty "box"
+ pretty AlignOf = pretty "alignof"
 
 instance Pretty BorrowKind where
  pretty = viaShow

crucible-mir/src/Mir/Trans.hs

@@ -578,19 +578,9 @@ transCheckedBinOp op a b = do
 
 -- Nullary ops in rust are used for resource allocation, so are not interpreted
 transNullaryOp :: M.NullOp -> M.Ty -> MirGenerator h s ret (MirExp s)
-transNullaryOp M.Box ty = do
- -- Box<T> has special translation to ensure that its representation is just
- -- an ordinary pointer.
- Some tpr <- tyToReprM ty
- ptr <- newMirRef tpr
- maybeInitVal <- initialValue ty
- case maybeInitVal of
- Just (MirExp tpr' initVal) -> do
- Refl <- testEqualityOrFail tpr tpr' $
- "bad initial value for box: expected " ++ show tpr ++ " but got " ++ show tpr'
- writeMirRef ptr initVal
- Nothing -> return ()
- return $ MirExp (MirReferenceRepr tpr) ptr
+transNullaryOp M.AlignOf ty = do
+ -- TODO: return the actual alignment
+ return $ MirExp UsizeRepr $ R.App $ usizeLit 4
 transNullaryOp M.SizeOf _ = do
  -- TODO: return the actual size, once mir-json exports size/layout info
  return $ MirExp UsizeRepr $ R.App $ usizeLit 1
@@ -983,6 +973,9 @@ evalRval rv@(M.RAdtAg (M.AdtAg adt agv ops ty)) = do
  mirFail $ "evalRval: Union types are unsupported, for " ++ show (adt ^. adtname)
  _ -> mirFail $ "evalRval: unsupported type for AdtAg: " ++ show ty
 
+-- TODO: are these correct?
+evalRval rv@(M.ShallowInitBox op ty) = evalOperand op
+evalRval rv@(M.CopyForDeref lv) = evalLvalue lv
 
 evalLvalue :: HasCallStack => M.Lvalue -> MirGenerator h s ret (MirExp s)
 evalLvalue lv = evalPlace lv >>= readPlace
@@ -1162,6 +1155,8 @@ transStatement (M.SetDiscriminant lv i) = do
  -- simultaneously), then we could remove AllocateEnum.
  ty -> mirFail $ "don't know how to set discriminant of " ++ show ty
 transStatement M.Nop = return ()
+transStatement M.Deinit = return ()
+transStatement (M.StmtIntrinsic _) = return () --TODO: is this true?
 
 -- | Add a new `BranchTransInfo` entry for the current function. Returns the
 -- index of the new entry.
@@ -1464,10 +1459,15 @@ transTerminator (M.DropAndReplace dlv dop dtarg _ dropFn) _ = do
  transStatement (M.Assign dlv (M.Use dop) "<dummy pos>")
  jumpToBlock dtarg
 
-transTerminator (M.Call (M.OpConstant (M.Constant _ (M.ConstFunction funid))) cargs cretdest _) tr = do
+-- transTerminator (M.Call (M.OpConstant (M.Constant _ (M.ConstFunction funid))) cargs cretdest _) tr = do
+-- isCustom <- resolveCustom funid
+-- doCall funid cargs cretdest tr -- cleanup ignored
+
+transTerminator (M.Call (M.OpConstant (M.Constant (M.TyFnDef funid) _)) cargs cretdest _) tr = do
  isCustom <- resolveCustom funid
  doCall funid cargs cretdest tr -- cleanup ignored
 
+
 transTerminator (M.Call funcOp cargs cretdest _) tr = do
  func <- evalOperand funcOp
  ret <- callHandle func RustAbi Nothing cargs

crucible-mir/src/Mir/TransTy.hs

@@ -325,7 +325,7 @@ reprTransparentFieldTy col adt = do
 
 
 variantFields :: TransTyConstraint => M.Collection -> M.Variant -> Some C.CtxRepr
-variantFields col (M.Variant _vn _vd vfs _vct) =
+variantFields col (M.Variant _vn _vd vfs _vct _mbVal) =
  tyReprListToCtx
  (map (mapSome fieldType . tyToFieldRepr col . (^. M.fty)) vfs)
  (\repr -> Some repr)
@@ -360,7 +360,7 @@ tyToFieldRepr col ty
  | otherwise = viewSome (\tpr -> Some $ FieldRepr $ FkMaybe tpr) (tyToRepr col ty)
 
 variantFields' :: TransTyConstraint => M.Collection -> M.Variant -> Some FieldCtxRepr
-variantFields' col (M.Variant _vn _vd vfs _vct) =
+variantFields' col (M.Variant _vn _vd vfs _vct _mbVal) =
  fieldReprListToCtx
  (map (tyToFieldRepr col . (^. M.fty)) vfs)
  (\x -> Some x)