Skip to content

Commit

Permalink
Nits in the JSON printer (#164)
Browse files Browse the repository at this point in the history 
* TypedExpr: nits in the JSON printer

* tests: regenerate tests output

* Update src/Syntax/TimeAgnostic.hs

Co-authored-by: sophierain <[email protected]>

* tests: regenerate tests output

* add JSON for storage and AbiType

* tests: regenerate tests output

---------

Co-authored-by: sophierain <[email protected]>
  • Loading branch information
@zoep @sophierain
zoep and sophierain authored Oct 12, 2023
1 parent 079f55c commit 2a9d345
Show file tree
Hide file tree
Showing 8 changed files with 3,325 additions and 1,794 deletions.
100 changes: 64 additions & 36 deletions src/Syntax/TimeAgnostic.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -352,24 +352,24 @@ instance Timable StorageRef where
-- It was difficult to construct a function with type:
-- `InvPredicate t -> Either (Exp Bool Timed,Exp Bool Timed) (Exp Bool Untimed)`
instance ToJSON (Act Timed) where
toJSON (Act storages contracts) = object [ "kind" .= String "Program"
toJSON (Act storages contracts) = object [ "kind" .= String "Act"
, "store" .= storeJSON storages
, "contracts" .= toJSON contracts ]

instance ToJSON (Act Untimed) where
toJSON (Act storages contracts) = object [ "kind" .= String "Program"
toJSON (Act storages contracts) = object [ "kind" .= String "Act"
, "store" .= storeJSON storages
, "contracts" .= toJSON contracts ]

instance ToJSON (Contract Timed) where
toJSON (Contract ctor behv) = object [ "kind" .= String "Contract"
, "constructor" .= toJSON ctor
, "behaviors" .= toJSON behv ]
, "constructor" .= toJSON ctor
, "behaviours" .= toJSON behv ]

instance ToJSON (Contract Untimed) where
toJSON (Contract ctor behv) = object [ "kind" .= String "Contract"
, "constructor" .= toJSON ctor
, "behaviors" .= toJSON behv ]
, "constructor" .= toJSON ctor
, "behaviours" .= toJSON behv ]


storeJSON :: Store -> Value
Expand All @@ -379,7 +379,7 @@ storeJSON storages = object [ "kind" .= String "Storages"
instance ToJSON (Constructor Timed) where
toJSON Constructor{..} = object [ "kind" .= String "Constructor"
, "contract" .= _cname
, "interface" .= (String . pack $ show _cinterface)
, "interface" .= toJSON _cinterface
, "preConditions" .= toJSON _cpreconditions
, "postConditions" .= toJSON _cpostconditions
, "invariants" .= listValue (\i@Invariant{..} -> invariantJSON i _predicate) _invariants
Expand All @@ -388,7 +388,7 @@ instance ToJSON (Constructor Timed) where
instance ToJSON (Constructor Untimed) where
toJSON Constructor{..} = object [ "kind" .= String "Constructor"
, "contract" .= _cname
, "interface" .= (String . pack $ show _cinterface)
, "interface" .= toJSON _cinterface
, "preConditions" .= toJSON _cpreconditions
, "postConditions" .= toJSON _cpostconditions
, "invariants" .= listValue (\i@Invariant{..} -> invariantJSON i _predicate) _invariants
Expand All @@ -398,13 +398,26 @@ instance ToJSON (Behaviour t) where
toJSON Behaviour{..} = object [ "kind" .= String "Behaviour"
, "name" .= _name
, "contract" .= _contract
, "interface" .= (String . pack $ show _interface)
, "interface" .= toJSON _interface
, "preConditions" .= toJSON _preconditions
, "case" .= toJSON _caseconditions
, "postConditions" .= toJSON _postconditions
, "stateUpdates" .= toJSON _stateUpdates
, "returns" .= toJSON _returns ]

instance ToJSON Interface where
toJSON (Interface x decls) = object [ "kind" .= String "Interface"
, "id" .= pack (show x)
, "args" .= toJSON decls
]

instance ToJSON Decl where
toJSON (Decl abitype x) = object [ "kind" .= String "Declaration"
, "id" .= pack (show x)
, "abitype" .= pack (show abitype)
]


invariantJSON :: ToJSON pred => Invariant t -> pred -> Value
invariantJSON Invariant{..} predicate = object [ "kind" .= String "Invariant"
, "predicate" .= toJSON predicate
Expand All @@ -413,8 +426,8 @@ invariantJSON Invariant{..} predicate = object [ "kind" .= String "Invariant"
, "contract" .= _icontract ]

instance ToJSON (Rewrite t) where
toJSON (Constant a) = object [ "Constant" .= toJSON a ]
toJSON (Rewrite a) = object [ "Rewrite" .= toJSON a ]
toJSON (Constant a) = object [ "constant" .= toJSON a ]
toJSON (Rewrite a) = object [ "rewrite" .= toJSON a ]

instance ToJSON (StorageLocation t) where
toJSON (Loc _ a) = object [ "location" .= toJSON a ]
Expand All @@ -423,26 +436,33 @@ instance ToJSON (StorageUpdate t) where
toJSON (Update _ a b) = object [ "location" .= toJSON a ,"value" .= toJSON b ]

instance ToJSON (TStorageItem a t) where
toJSON (Item t _ a) = object [ "sort" .= pack (show t)
, "item" .= toJSON a ]
toJSON (Item t _ a) = object [ "item" .= toJSON a
, "type" .= show t
]

instance ToJSON (StorageRef t) where
toJSON (SVar _ c x) = object [ "var" .= String (pack c <> "." <> pack x) ]
toJSON (SVar _ c x) = object [ "kind" .= pack "SVar"
, "svar" .= pack x
, "contract" .= pack c ]
toJSON (SMapping _ e xs) = mapping e xs
toJSON (SField _ e _ x) = field e x
toJSON (SField _ e c x) = field e c x

mapping :: (ToJSON a1, ToJSON a2) => a1 -> a2 -> Value
mapping a b = object [ "symbol" .= pack "lookup"
, "arity" .= Data.Aeson.Types.Number 2
, "args" .= Array (fromList [toJSON a, toJSON b]) ]
mapping a b = object [ "kind" .= pack "Mapping"
, "indexes" .= toJSON b
, "reference" .= toJSON a]

field :: (ToJSON a1) => a1 -> Id -> Id -> Value
field a c x = object [ "kind" .= pack "Field"
, "field" .= pack x
, "contract" .= pack c
, "reference" .= toJSON a
]

field :: (ToJSON a1, ToJSON a2) => a1 -> a2 -> Value
field a b = object [ "symbol" .= pack "select"
, "arity" .= Data.Aeson.Types.Number 2
, "args" .= Array (fromList [toJSON a, toJSON b]) ]

instance ToJSON (TypedExp t) where
toJSON (TExp typ a) = object [ "sort" .= pack (show typ)
toJSON (TExp typ a) = object [ "kind" .= pack "TypedExpr"
, "type" .= pack (show typ)
, "expression" .= toJSON a ]

instance ToJSON (Exp a t) where
Expand All @@ -451,14 +471,15 @@ instance ToJSON (Exp a t) where
toJSON (Exp _ a b) = symbol "^" a b
toJSON (Mul _ a b) = symbol "*" a b
toJSON (Div _ a b) = symbol "/" a b
toJSON (LitInt _ a) = toJSON $ show a
toJSON (LitInt _ a) = object [ "literal" .= pack (show a)
, "type" .= pack "int" ]
toJSON (IntMin _ a) = toJSON $ show $ intmin a
toJSON (IntMax _ a) = toJSON $ show $ intmax a
toJSON (UIntMin _ a) = toJSON $ show $ uintmin a
toJSON (UIntMax _ a) = toJSON $ show $ uintmax a
toJSON (InRange _ a b) = object [ "symbol" .= pack ("inrange" <> show a)
, "arity" .= Data.Aeson.Types.Number 1
, "args" .= Array (fromList [toJSON b]) ]
toJSON (InRange _ a b) = object [ "symbol" .= pack "inrange"
, "arity" .= Data.Aeson.Types.Number 2
, "args" .= Array (fromList [String (pack $ show a), toJSON b]) ]
toJSON (IntEnv _ a) = String $ pack $ show a
toJSON (ITE _ a b c) = object [ "symbol" .= pack "ite"
, "arity" .= Data.Aeson.Types.Number 3
Expand All @@ -472,7 +493,8 @@ instance ToJSON (Exp a t) where
toJSON (Eq _ _ a b) = symbol "==" a b
toJSON (LEQ _ a b) = symbol "<=" a b
toJSON (GEQ _ a b) = symbol ">=" a b
toJSON (LitBool _ a) = String $ pack $ show a
toJSON (LitBool _ a) = object [ "literal" .= pack (show a)
, "type" .= pack "bool" ]
toJSON (Neg _ a) = object [ "symbol" .= pack "not"
, "arity" .= Data.Aeson.Types.Number 1
, "args" .= Array (fromList [toJSON a]) ]
Expand All @@ -481,18 +503,24 @@ instance ToJSON (Exp a t) where
toJSON (Slice _ s a b) = object [ "symbol" .= pack "slice"
, "arity" .= Data.Aeson.Types.Number 3
, "args" .= Array (fromList [toJSON s, toJSON a, toJSON b]) ]
toJSON (ByStr _ a) = toJSON a
toJSON (ByLit _ a) = String . pack $ show a
toJSON (ByEnv _ a) = String . pack $ show a

toJSON (TEntry _ t a) = object [ fromString (show t) .= toJSON a ]
toJSON (Var _ _ _ a) = toJSON a
toJSON (ByStr _ a) = object [ "bytestring" .= toJSON a
, "type" .= pack "bool" ]
toJSON (ByLit _ a) = object [ "literal" .= pack (show a)
, "type" .= pack "bytestring" ]
toJSON (ByEnv _ a) = object [ "ethEnv" .= pack (show a)
, "type" .= pack "bytestring" ]
toJSON (TEntry _ t a) = object [ "entry" .= toJSON a
, "timing" .= show t ]
toJSON (Var _ t _ a) = object [ "var" .= toJSON a
, "type" .= show t ]
toJSON (Create _ f xs) = object [ "symbol" .= pack "create"
, "arity" .= Data.Aeson.Types.Number 2
, "args" .= Array (fromList [object [ "fun" .= String (pack f) ], toJSON xs]) ]
, "arity" .= Data.Aeson.Types.Number 2
, "args" .= Array (fromList [object [ "fun" .= String (pack f) ], toJSON xs]) ]

toJSON v = error $ "todo: json ast for: " <> show v



symbol :: (ToJSON a1, ToJSON a2) => String -> a1 -> a2 -> Value
symbol s a b = object [ "symbol" .= pack s
, "arity" .= Data.Aeson.Types.Number 2
Expand Down
45 changes: 39 additions & 6 deletions src/Syntax/Untyped.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,10 @@ module Syntax.Untyped (module Syntax.Untyped) where

import Data.Aeson
import Data.List (intercalate)
import Data.List.NonEmpty (toList, NonEmpty)
import Data.List.NonEmpty (NonEmpty)
import Data.Text as T (pack)

import EVM.ABI (AbiType)
import EVM.ABI (AbiType(..))
import Lex

type Pn = AlexPosn
Expand Down Expand Up @@ -154,6 +155,7 @@ instance Show SlotType where
<> ")")
(show t) s


data StorageVar = StorageVar Pn SlotType Id
deriving (Eq, Show)

Expand All @@ -164,10 +166,41 @@ instance Show Decl where
show (Decl t a) = show t <> " " <> a

instance ToJSON SlotType where
toJSON (StorageValue t) = object ["type" .= show t]
toJSON (StorageMapping ixTypes valType) = object [ "type" .= String "mapping"
, "ixTypes" .= show (toList ixTypes)
, "valType" .= show valType]
toJSON (StorageValue t) = object ["kind" .= String "ValueType"
, "valueType" .= toJSON t]
toJSON (StorageMapping ixTypes resType) = object [ "kind" .= String "MappingType"
, "ixTypes" .= toJSON ixTypes
, "resType" .= toJSON resType]


instance ToJSON ValueType where
toJSON (ContractType c) = object [ "kind" .= String "ContractType"
, "name" .= show c ]
toJSON (PrimitiveType abiType) = object [ "kind" .= String "AbiType"
, "abiType" .= toJSON abiType ]


instance ToJSON AbiType where
toJSON (AbiUIntType n) = object [ "type" .= String "UInt"
, "size" .= String (T.pack $ show n) ]
toJSON (AbiIntType n) = object [ "type" .= String "Int"
, "size" .= String (T.pack $ show n) ]
toJSON AbiAddressType = object [ "type" .= String "Address" ]
toJSON AbiBoolType = object [ "type" .= String "Bool" ]
toJSON (AbiBytesType n) = object [ "type" .= String "Bytes"
, "size" .= String (T.pack $ show n) ]
toJSON AbiBytesDynamicType = object [ "type" .= String "BytesDynamic" ]
toJSON AbiStringType = object [ "type" .= String "String" ]
toJSON (AbiArrayDynamicType t) = object [ "type" .= String "ArrayDynamic"
, "arrayType" .= toJSON t ]
toJSON (AbiArrayType n t) = object [ "type" .= String "Array"
, "arrayType" .= toJSON t
, "size" .= String (T.pack $ show n) ]
toJSON (AbiTupleType ts) = object [ "type" .= String "Tuple"
, "elemTypes" .= toJSON ts ]
toJSON (AbiFunctionType) = object [ "type" .= String "Function" ]



-- Create the string that is used to construct the function selector
makeIface :: Interface -> String
Expand Down
Loading

0 comments on commit 2a9d345

Please sign in to comment.