Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Nits in the JSON printer #164

Merged
merged 6 commits into from
Oct 12, 2023
Merged

Nits in the JSON printer #164

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
f644ee6
TypedExpr: nits in the JSON printer
zoep Oct 10, 2023
8410734
tests: regenerate tests output
zoep Oct 10, 2023
34d4c85
Update src/Syntax/TimeAgnostic.hs
zoep Oct 11, 2023
c8428f1
tests: regenerate tests output
zoep Oct 11, 2023
548ddc7
add JSON for storage and AbiType
zoep Oct 11, 2023
d3b1b62
tests: regenerate tests output
zoep Oct 11, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
100 changes: 64 additions & 36 deletions src/Syntax/TimeAgnostic.hs
View file
Open in desktop
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
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Print int min-max as literals

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
Open in desktop
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
Loading