From f644ee666486209371acb2cd971d622f0fcfcc69 Mon Sep 17 00:00:00 2001 From: zoep Date: Tue, 10 Oct 2023 21:02:40 +0300 Subject: [PATCH 1/6] TypedExpr: nits in the JSON printer --- src/Syntax/TimeAgnostic.hs | 100 ++++++++++++++++++++++++------------- 1 file changed, 64 insertions(+), 36 deletions(-) diff --git a/src/Syntax/TimeAgnostic.hs b/src/Syntax/TimeAgnostic.hs index 0f974e7e..5db4c762 100644 --- a/src/Syntax/TimeAgnostic.hs +++ b/src/Syntax/TimeAgnostic.hs @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 ] @@ -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" + , "sort" .= pack (show typ) , "expression" .= toJSON a ] instance ToJSON (Exp a t) where @@ -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 @@ -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]) ] @@ -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 From 8410734b67488e992110ed8eba9c612ae38ea219 Mon Sep 17 00:00:00 2001 From: zoep Date: Tue, 10 Oct 2023 22:16:40 +0300 Subject: [PATCH 2/6] tests: regenerate tests output --- tests/frontend/pass/case/case.act.typed.json | 292 +- .../pass/creation/create.act.typed.json | 32 +- .../frontend/pass/multi/multi.act.typed.json | 322 +- .../pass/safemath/safemathraw.act.typed.json | 118 +- .../frontend/pass/smoke/smoke.act.typed.json | 48 +- .../pass/token/transfer.act.typed.json | 4031 +++++++++++------ 6 files changed, 3112 insertions(+), 1731 deletions(-) diff --git a/tests/frontend/pass/case/case.act.typed.json b/tests/frontend/pass/case/case.act.typed.json index bf8909fc..80c5425d 100644 --- a/tests/frontend/pass/case/case.act.typed.json +++ b/tests/frontend/pass/case/case.act.typed.json @@ -1,20 +1,36 @@ { "contracts": [ { - "behaviors": [ + "behaviours": [ { "case": [ { "args": [ - "z", - "0" + { + "type": "int", + "var": "z" + }, + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" } ], "contract": "C", - "interface": "bar(uint256 z)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"z\"", + "kind": "Declaration" + } + ], + "id": "\"bar\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "bar", "postConditions": [], @@ -22,7 +38,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -31,15 +50,24 @@ "args": [ { "args": [ - "0", - "z" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "z" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "z", + { + "type": "int", + "var": "z" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -53,14 +81,20 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -69,12 +103,15 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -89,7 +126,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -111,14 +151,19 @@ "returns": null, "stateUpdates": [ { - "Rewrite": { + "rewrite": { "location": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" + "type": "int" }, - "value": "z" + "value": { + "type": "int", + "var": "z" + } } } ] @@ -127,15 +172,31 @@ "case": [ { "args": [ - "z", - "1" + { + "type": "int", + "var": "z" + }, + { + "literal": "1", + "type": "int" + } ], "arity": 2, "symbol": "==" } ], "contract": "C", - "interface": "bar(uint256 z)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"z\"", + "kind": "Declaration" + } + ], + "id": "\"bar\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "bar", "postConditions": [], @@ -143,7 +204,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -152,15 +216,24 @@ "args": [ { "args": [ - "0", - "z" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "z" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "z", + { + "type": "int", + "var": "z" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -174,14 +247,20 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -190,12 +269,15 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -210,7 +292,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -232,17 +317,25 @@ "returns": null, "stateUpdates": [ { - "Rewrite": { + "rewrite": { "location": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" + "type": "int" }, "value": { "args": [ - "z", - "1" + { + "type": "int", + "var": "z" + }, + { + "literal": "1", + "type": "int" + } ], "arity": 2, "symbol": "+" @@ -255,15 +348,31 @@ "case": [ { "args": [ - "z", - "1" + { + "type": "int", + "var": "z" + }, + { + "literal": "1", + "type": "int" + } ], "arity": 2, "symbol": ">" } ], "contract": "C", - "interface": "bar(uint256 z)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"z\"", + "kind": "Declaration" + } + ], + "id": "\"bar\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "bar", "postConditions": [], @@ -271,7 +380,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -280,15 +392,24 @@ "args": [ { "args": [ - "0", - "z" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "z" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "z", + { + "type": "int", + "var": "z" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -302,14 +423,20 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -318,12 +445,15 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -338,7 +468,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -360,17 +493,25 @@ "returns": null, "stateUpdates": [ { - "Rewrite": { + "rewrite": { "location": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" + "type": "int" }, "value": { "args": [ - "z", - "2" + { + "type": "int", + "var": "z" + }, + { + "literal": "2", + "type": "int" + } ], "arity": 2, "symbol": "+" @@ -386,14 +527,23 @@ { "location": { "item": { - "var": "C.x" + "contract": "C", + "kind": "SVar", + "svar": "x" }, - "sort": "int" + "type": "int" }, - "value": "0" + "value": { + "literal": "0", + "type": "int" + } } ], - "interface": "C()", + "interface": { + "args": [], + "id": "\"C\"", + "kind": "Interface" + }, "invariants": [], "kind": "Constructor", "postConditions": [], @@ -402,7 +552,7 @@ "kind": "Contract" } ], - "kind": "Program", + "kind": "Act", "store": { "kind": "Storages", "storages": { diff --git a/tests/frontend/pass/creation/create.act.typed.json b/tests/frontend/pass/creation/create.act.typed.json index 240692e8..00bd0a7b 100644 --- a/tests/frontend/pass/creation/create.act.typed.json +++ b/tests/frontend/pass/creation/create.act.typed.json @@ -1,30 +1,41 @@ { "contracts": [ { - "behaviors": [], + "behaviours": [], "constructor": { "contract": "Modest", "initial storage": [ { "location": { "item": { - "var": "Modest.x" + "contract": "Modest", + "kind": "SVar", + "svar": "x" }, - "sort": "int" + "type": "int" }, - "value": "1" + "value": { + "literal": "1", + "type": "int" + } }, { "location": { "item": { - "var": "Modest.y" + "contract": "Modest", + "kind": "SVar", + "svar": "y" }, - "sort": "int" + "type": "int" }, "value": "Caller" } ], - "interface": "Modest()", + "interface": { + "args": [], + "id": "\"Modest\"", + "kind": "Interface" + }, "invariants": [], "kind": "Constructor", "postConditions": [], @@ -33,7 +44,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -56,7 +70,7 @@ "kind": "Contract" } ], - "kind": "Program", + "kind": "Act", "store": { "kind": "Storages", "storages": { diff --git a/tests/frontend/pass/multi/multi.act.typed.json b/tests/frontend/pass/multi/multi.act.typed.json index c8ceeaed..d801319e 100644 --- a/tests/frontend/pass/multi/multi.act.typed.json +++ b/tests/frontend/pass/multi/multi.act.typed.json @@ -1,21 +1,30 @@ { "contracts": [ { - "behaviors": [], + "behaviours": [], "constructor": { "contract": "A", "initial storage": [ { "location": { "item": { - "var": "A.x" + "contract": "A", + "kind": "SVar", + "svar": "x" }, - "sort": "int" + "type": "int" }, - "value": "0" + "value": { + "literal": "0", + "type": "int" + } } ], - "interface": "A()", + "interface": { + "args": [], + "id": "\"A\"", + "kind": "Interface" + }, "invariants": [], "kind": "Constructor", "postConditions": [], @@ -24,13 +33,26 @@ "kind": "Contract" }, { - "behaviors": [ + "behaviours": [ { "case": [ - "True" + { + "literal": "True", + "type": "bool" + } ], "contract": "B", - "interface": "set_remote(uint256 z)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"z\"", + "kind": "Declaration" + } + ], + "id": "\"set_remote\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "remote", "postConditions": [], @@ -38,7 +60,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -47,15 +72,24 @@ "args": [ { "args": [ - "0", - "z" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "z" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "z", + { + "type": "int", + "var": "z" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -69,21 +103,25 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ - { - "var": "B.a" - }, - "x" - ], - "arity": 2, - "symbol": "select" + "contract": "A", + "field": "x", + "kind": "Field", + "reference": { + "contract": "B", + "kind": "SVar", + "svar": "a" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -92,19 +130,20 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ - { - "var": "B.a" - }, - "x" - ], - "arity": 2, - "symbol": "select" + "contract": "A", + "field": "x", + "kind": "Field", + "reference": { + "contract": "B", + "kind": "SVar", + "svar": "a" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -119,7 +158,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -141,31 +183,47 @@ "returns": null, "stateUpdates": [ { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ - { - "var": "B.a" - }, - "x" - ], - "arity": 2, - "symbol": "select" + "contract": "A", + "field": "x", + "kind": "Field", + "reference": { + "contract": "B", + "kind": "SVar", + "svar": "a" + } }, - "sort": "int" + "type": "int" }, - "value": "z" + "value": { + "type": "int", + "var": "z" + } } } ] }, { "case": [ - "True" + { + "literal": "True", + "type": "bool" + } ], "contract": "B", - "interface": "set_remote2(uint256 z)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"z\"", + "kind": "Declaration" + } + ], + "id": "\"set_remote2\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "multi", "postConditions": [], @@ -173,7 +231,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -182,15 +243,24 @@ "args": [ { "args": [ - "0", - "z" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "z" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "z", + { + "type": "int", + "var": "z" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -204,14 +274,20 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "var": "B.y" + "contract": "B", + "kind": "SVar", + "svar": "y" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -220,12 +296,15 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "B.y" + "contract": "B", + "kind": "SVar", + "svar": "y" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -240,21 +319,25 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ - { - "var": "B.a" - }, - "x" - ], - "arity": 2, - "symbol": "select" + "contract": "A", + "field": "x", + "kind": "Field", + "reference": { + "contract": "B", + "kind": "SVar", + "svar": "a" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -263,19 +346,20 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ - { - "var": "B.a" - }, - "x" - ], - "arity": 2, - "symbol": "select" + "contract": "A", + "field": "x", + "kind": "Field", + "reference": { + "contract": "B", + "kind": "SVar", + "svar": "a" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -290,7 +374,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -312,32 +399,40 @@ "returns": null, "stateUpdates": [ { - "Rewrite": { + "rewrite": { "location": { "item": { - "var": "B.y" + "contract": "B", + "kind": "SVar", + "svar": "y" }, - "sort": "int" + "type": "int" }, - "value": "1" + "value": { + "literal": "1", + "type": "int" + } } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ - { - "var": "B.a" - }, - "x" - ], - "arity": 2, - "symbol": "select" + "contract": "A", + "field": "x", + "kind": "Field", + "reference": { + "contract": "B", + "kind": "SVar", + "svar": "a" + } }, - "sort": "int" + "type": "int" }, - "value": "z" + "value": { + "type": "int", + "var": "z" + } } } ] @@ -349,18 +444,25 @@ { "location": { "item": { - "var": "B.y" + "contract": "B", + "kind": "SVar", + "svar": "y" }, - "sort": "int" + "type": "int" }, - "value": "0" + "value": { + "literal": "0", + "type": "int" + } }, { "location": { "item": { - "var": "B.a" + "contract": "B", + "kind": "SVar", + "svar": "a" }, - "sort": "contract" + "type": "contract" }, "value": { "args": [ @@ -374,7 +476,11 @@ } } ], - "interface": "B()", + "interface": { + "args": [], + "id": "\"B\"", + "kind": "Interface" + }, "invariants": [], "kind": "Constructor", "postConditions": [], @@ -383,7 +489,7 @@ "kind": "Contract" } ], - "kind": "Program", + "kind": "Act", "store": { "kind": "Storages", "storages": { diff --git a/tests/frontend/pass/safemath/safemathraw.act.typed.json b/tests/frontend/pass/safemath/safemathraw.act.typed.json index ae223cda..07364294 100644 --- a/tests/frontend/pass/safemath/safemathraw.act.typed.json +++ b/tests/frontend/pass/safemath/safemathraw.act.typed.json @@ -1,49 +1,85 @@ { "contracts": [ { - "behaviors": [ + "behaviours": [ { "case": [ - "True" + { + "literal": "True", + "type": "bool" + } ], "contract": "SafeAdd", - "interface": "add(uint256 x, uint256 y)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"x\"", + "kind": "Declaration" + }, + { + "abitype": "uint256", + "id": "\"y\"", + "kind": "Declaration" + } + ], + "id": "\"add\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "add", "postConditions": [], "preConditions": [ { "args": [ + "uint256", { "args": [ - "x", - "y" + { + "type": "int", + "var": "x" + }, + { + "type": "int", + "var": "y" + } ], "arity": 2, "symbol": "+" } ], - "arity": 1, - "symbol": "inrangeuint256" + "arity": 2, + "symbol": "inrange" }, { "args": [ - "x" + "uint256", + { + "type": "int", + "var": "x" + } ], - "arity": 1, - "symbol": "inrangeuint256" + "arity": 2, + "symbol": "inrange" }, { "args": [ - "y" + "uint256", + { + "type": "int", + "var": "y" + } ], - "arity": 1, - "symbol": "inrangeuint256" + "arity": 2, + "symbol": "inrange" }, { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -52,15 +88,24 @@ "args": [ { "args": [ - "0", - "x" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "x" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "x", + { + "type": "int", + "var": "x" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -74,15 +119,24 @@ "args": [ { "args": [ - "0", - "y" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "y" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "y", + { + "type": "int", + "var": "y" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -96,7 +150,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -118,12 +175,19 @@ "returns": { "expression": { "args": [ - "x", - "y" + { + "type": "int", + "var": "x" + }, + { + "type": "int", + "var": "y" + } ], "arity": 2, "symbol": "+" }, + "kind": "TypedExpr", "sort": "int" }, "stateUpdates": [] @@ -132,7 +196,11 @@ "constructor": { "contract": "SafeAdd", "initial storage": [], - "interface": "SafeAdd()", + "interface": { + "args": [], + "id": "\"SafeAdd\"", + "kind": "Interface" + }, "invariants": [], "kind": "Constructor", "postConditions": [], @@ -141,7 +209,7 @@ "kind": "Contract" } ], - "kind": "Program", + "kind": "Act", "store": { "kind": "Storages", "storages": { diff --git a/tests/frontend/pass/smoke/smoke.act.typed.json b/tests/frontend/pass/smoke/smoke.act.typed.json index d3dbbf40..c7a534b8 100644 --- a/tests/frontend/pass/smoke/smoke.act.typed.json +++ b/tests/frontend/pass/smoke/smoke.act.typed.json @@ -1,13 +1,26 @@ { "contracts": [ { - "behaviors": [ + "behaviours": [ { "case": [ - "True" + { + "literal": "True", + "type": "bool" + } ], "contract": "A", - "interface": "f(uint256 x)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"x\"", + "kind": "Declaration" + } + ], + "id": "\"f\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "f", "postConditions": [], @@ -16,15 +29,24 @@ "args": [ { "args": [ - "0", - "x" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "x" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "x", + { + "type": "int", + "var": "x" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -36,7 +58,11 @@ } ], "returns": { - "expression": "1", + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", "sort": "int" }, "stateUpdates": [] @@ -45,7 +71,11 @@ "constructor": { "contract": "A", "initial storage": [], - "interface": "A()", + "interface": { + "args": [], + "id": "\"A\"", + "kind": "Interface" + }, "invariants": [], "kind": "Constructor", "postConditions": [], @@ -54,7 +84,7 @@ "kind": "Contract" } ], - "kind": "Program", + "kind": "Act", "store": { "kind": "Storages", "storages": { diff --git a/tests/frontend/pass/token/transfer.act.typed.json b/tests/frontend/pass/token/transfer.act.typed.json index 019e7070..02345498 100644 --- a/tests/frontend/pass/token/transfer.act.typed.json +++ b/tests/frontend/pass/token/transfer.act.typed.json @@ -1,20 +1,38 @@ { "contracts": [ { - "behaviors": [ + "behaviours": [ { "case": [ { "args": [ "Caller", - "to" + { + "type": "int", + "var": "to" + } ], "arity": 2, "symbol": "=/=" } ], "contract": "Token", - "interface": "transfer(uint256 value, address to)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"value\"", + "kind": "Declaration" + }, + { + "abitype": "address", + "id": "\"to\"", + "kind": "Declaration" + } + ], + "id": "\"transfer\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "transfer", "postConditions": [], @@ -22,33 +40,40 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" }, { "args": [ - "value", { - "Pre": { + "type": "int", + "var": "value" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -59,7 +84,10 @@ { "args": [ "Caller", - "to" + { + "type": "int", + "var": "to" + } ], "arity": 2, "symbol": "=/=" @@ -69,34 +97,47 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "value" + { + "type": "int", + "var": "value" + } ], "arity": 2, "symbol": "+" }, { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" @@ -113,15 +154,24 @@ "args": [ { "args": [ - "0", - "value" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "value" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "value", + { + "type": "int", + "var": "value" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -135,15 +185,24 @@ "args": [ { "args": [ - "0", - "to" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "to" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "to", + { + "type": "int", + "var": "to" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -157,26 +216,30 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -185,24 +248,25 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -217,26 +281,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -245,24 +316,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -277,7 +352,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -299,7 +377,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -319,53 +400,61 @@ } ], "returns": { - "expression": "1", + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", "sort": "int" }, "stateUpdates": [ { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "value" + { + "type": "int", + "var": "value" + } ], "arity": 2, "symbol": "-" @@ -373,48 +462,58 @@ } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "value" + { + "type": "int", + "var": "value" + } ], "arity": 2, "symbol": "+" @@ -428,14 +527,32 @@ { "args": [ "Caller", - "to" + { + "type": "int", + "var": "to" + } ], "arity": 2, "symbol": "==" } ], "contract": "Token", - "interface": "transfer(uint256 value, address to)", + "interface": { + "args": [ + { + "abitype": "uint256", + "id": "\"value\"", + "kind": "Declaration" + }, + { + "abitype": "address", + "id": "\"to\"", + "kind": "Declaration" + } + ], + "id": "\"transfer\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "transfer", "postConditions": [], @@ -443,33 +560,40 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" }, { "args": [ - "value", { - "Pre": { + "type": "int", + "var": "value" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -480,7 +604,10 @@ { "args": [ "Caller", - "to" + { + "type": "int", + "var": "to" + } ], "arity": 2, "symbol": "=/=" @@ -490,34 +617,47 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "value" + { + "type": "int", + "var": "value" + } ], "arity": 2, "symbol": "+" }, { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" @@ -534,15 +674,24 @@ "args": [ { "args": [ - "0", - "value" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "value" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "value", + { + "type": "int", + "var": "value" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -556,15 +705,24 @@ "args": [ { "args": [ - "0", - "to" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "to" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "to", + { + "type": "int", + "var": "to" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -578,26 +736,30 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -606,24 +768,25 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -638,26 +801,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -666,24 +836,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -698,7 +872,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -720,7 +897,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -740,51 +920,58 @@ } ], "returns": { - "expression": "1", + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", "sort": "int" }, "stateUpdates": [ { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } }, { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "to", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "to" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } } @@ -796,8 +983,14 @@ "args": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "=/=" @@ -805,7 +998,10 @@ { "args": [ "Caller", - "src" + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "==" @@ -816,33 +1012,57 @@ } ], "contract": "Token", - "interface": "transferFrom(address src, address dst, uint256 amount)", - "kind": "Behaviour", - "name": "transferFrom", - "postConditions": [], - "preConditions": [ - { + "interface": { + "args": [ + { + "abitype": "address", + "id": "\"src\"", + "kind": "Declaration" + }, + { + "abitype": "address", + "id": "\"dst\"", + "kind": "Declaration" + }, + { + "abitype": "uint256", + "id": "\"amount\"", + "kind": "Declaration" + } + ], + "id": "\"transferFrom\"", + "kind": "Interface" + }, + "kind": "Behaviour", + "name": "transferFrom", + "postConditions": [], + "preConditions": [ + { "args": [ - "amount", { - "Pre": { + "type": "int", + "var": "amount" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -852,8 +1072,14 @@ "args": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "=/=" @@ -863,34 +1089,47 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "+" }, { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" @@ -908,41 +1147,55 @@ { "args": [ "Caller", - "src" + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "=/=" }, { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -958,7 +1211,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -967,15 +1223,24 @@ "args": [ { "args": [ - "0", - "src" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "src", + { + "type": "int", + "var": "src" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -989,15 +1254,24 @@ "args": [ { "args": [ - "0", - "dst" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "dst", + { + "type": "int", + "var": "dst" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -1011,15 +1285,24 @@ "args": [ { "args": [ - "0", - "amount" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "amount", + { + "type": "int", + "var": "amount" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -1033,26 +1316,30 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1061,24 +1348,25 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -1093,30 +1381,38 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1125,28 +1421,33 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -1161,26 +1462,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1189,24 +1497,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -1221,26 +1533,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1249,24 +1568,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -1281,7 +1604,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -1303,7 +1629,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -1323,101 +1652,119 @@ } ], "returns": { - "expression": "1", + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", "sort": "int" }, "stateUpdates": [ { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } }, { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" + "type": "int" } } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -1425,48 +1772,58 @@ } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "+" @@ -1483,8 +1840,14 @@ "args": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "=/=" @@ -1492,7 +1855,10 @@ { "args": [ "Caller", - "src" + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "=/=" @@ -1504,40 +1870,54 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, { "args": [ { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" }, - "1" + { + "literal": "1", + "type": "int" + } ], "arity": 2, "symbol": "-" @@ -1552,33 +1932,57 @@ } ], "contract": "Token", - "interface": "transferFrom(address src, address dst, uint256 amount)", + "interface": { + "args": [ + { + "abitype": "address", + "id": "\"src\"", + "kind": "Declaration" + }, + { + "abitype": "address", + "id": "\"dst\"", + "kind": "Declaration" + }, + { + "abitype": "uint256", + "id": "\"amount\"", + "kind": "Declaration" + } + ], + "id": "\"transferFrom\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "transferFrom", "postConditions": [], "preConditions": [ { "args": [ - "amount", { - "Pre": { + "type": "int", + "var": "amount" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1588,8 +1992,14 @@ "args": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "=/=" @@ -1599,34 +2009,47 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "+" }, { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" @@ -1644,41 +2067,55 @@ { "args": [ "Caller", - "src" + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "=/=" }, { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -1694,7 +2131,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -1703,15 +2143,24 @@ "args": [ { "args": [ - "0", - "src" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "src", + { + "type": "int", + "var": "src" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -1725,15 +2174,24 @@ "args": [ { "args": [ - "0", - "dst" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "dst", + { + "type": "int", + "var": "dst" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -1747,15 +2205,24 @@ "args": [ { "args": [ - "0", - "amount" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "amount", + { + "type": "int", + "var": "amount" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -1769,26 +2236,30 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1797,24 +2268,25 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -1829,30 +2301,38 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1861,28 +2341,33 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -1897,26 +2382,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1925,24 +2417,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -1957,26 +2453,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -1985,24 +2488,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -2017,7 +2524,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -2039,7 +2549,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -2059,101 +2572,119 @@ } ], "returns": { - "expression": "1", + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", "sort": "int" }, "stateUpdates": [ { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } }, { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" + "type": "int" } } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -2161,48 +2692,58 @@ } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "+" @@ -2219,8 +2760,14 @@ "args": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "=/=" @@ -2228,7 +2775,10 @@ { "args": [ "Caller", - "src" + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "=/=" @@ -2240,40 +2790,54 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, { "args": [ { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" }, - "1" + { + "literal": "1", + "type": "int" + } ], "arity": 2, "symbol": "-" @@ -2288,33 +2852,57 @@ } ], "contract": "Token", - "interface": "transferFrom(address src, address dst, uint256 amount)", + "interface": { + "args": [ + { + "abitype": "address", + "id": "\"src\"", + "kind": "Declaration" + }, + { + "abitype": "address", + "id": "\"dst\"", + "kind": "Declaration" + }, + { + "abitype": "uint256", + "id": "\"amount\"", + "kind": "Declaration" + } + ], + "id": "\"transferFrom\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "transferFrom", "postConditions": [], "preConditions": [ { "args": [ - "amount", { - "Pre": { + "type": "int", + "var": "amount" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -2324,8 +2912,14 @@ "args": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "=/=" @@ -2335,34 +2929,47 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "+" }, { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" @@ -2380,41 +2987,55 @@ { "args": [ "Caller", - "src" + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "=/=" }, { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -2430,7 +3051,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -2439,15 +3063,24 @@ "args": [ { "args": [ - "0", - "src" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "src", + { + "type": "int", + "var": "src" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -2461,15 +3094,24 @@ "args": [ { "args": [ - "0", - "dst" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "dst", + { + "type": "int", + "var": "dst" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -2483,15 +3125,24 @@ "args": [ { "args": [ - "0", - "amount" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "amount", + { + "type": "int", + "var": "amount" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -2505,26 +3156,30 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -2533,24 +3188,25 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -2565,30 +3221,38 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -2597,28 +3261,33 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -2633,26 +3302,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -2661,24 +3337,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -2693,26 +3373,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -2721,24 +3408,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -2753,7 +3444,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -2775,7 +3469,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -2795,83 +3492,99 @@ } ], "returns": { - "expression": "1", + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", "sort": "int" }, "stateUpdates": [ { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -2879,48 +3592,58 @@ } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -2928,48 +3651,58 @@ } }, { - "Rewrite": { + "rewrite": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, "value": { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "+" @@ -2982,41 +3715,71 @@ "case": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "==" } ], "contract": "Token", - "interface": "transferFrom(address src, address dst, uint256 amount)", + "interface": { + "args": [ + { + "abitype": "address", + "id": "\"src\"", + "kind": "Declaration" + }, + { + "abitype": "address", + "id": "\"dst\"", + "kind": "Declaration" + }, + { + "abitype": "uint256", + "id": "\"amount\"", + "kind": "Declaration" + } + ], + "id": "\"transferFrom\"", + "kind": "Interface" + }, "kind": "Behaviour", "name": "transferFrom", "postConditions": [], "preConditions": [ { "args": [ - "amount", { - "Pre": { + "type": "int", + "var": "amount" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -3026,8 +3789,14 @@ "args": [ { "args": [ - "src", - "dst" + { + "type": "int", + "var": "src" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "=/=" @@ -3037,34 +3806,47 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "+" }, { "args": [ - "2", - "256" + { + "literal": "2", + "type": "int" + }, + { + "literal": "256", + "type": "int" + } ], "arity": 2, "symbol": "^" @@ -3082,41 +3864,55 @@ { "args": [ "Caller", - "src" + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "=/=" }, { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "amount" + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "-" @@ -3132,7 +3928,10 @@ { "args": [ "Callvalue", - "0" + { + "literal": "0", + "type": "int" + } ], "arity": 2, "symbol": "==" @@ -3141,15 +3940,24 @@ "args": [ { "args": [ - "0", - "src" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "src" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "src", + { + "type": "int", + "var": "src" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -3163,15 +3971,24 @@ "args": [ { "args": [ - "0", - "dst" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "dst" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "dst", + { + "type": "int", + "var": "dst" + }, "1461501637330902918203684832716283019655932542975" ], "arity": 2, @@ -3185,15 +4002,24 @@ "args": [ { "args": [ - "0", - "amount" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "amount" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "amount", + { + "type": "int", + "var": "amount" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -3207,26 +4033,30 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -3235,24 +4065,25 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -3267,30 +4098,38 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -3299,28 +4138,33 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -3335,26 +4179,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -3363,24 +4214,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -3395,26 +4250,33 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -3423,24 +4285,28 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -3455,7 +4321,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -3477,7 +4346,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Callvalue" ], "arity": 2, @@ -3497,99 +4369,113 @@ } ], "returns": { - "expression": "1", + "expression": { + "literal": "1", + "type": "int" + }, + "kind": "TypedExpr", "sort": "int" }, "stateUpdates": [ { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } }, { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.allowance" - }, - [ - { - "expression": "src", - "sort": "int" + "expression": { + "type": "int", + "var": "src" }, - { - "expression": "Caller", - "sort": "int" - } - ] + "kind": "TypedExpr", + "sort": "int" + }, + { + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "allowance" + } }, - "sort": "int" + "type": "int" } } }, { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "src", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "src" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } }, { - "Constant": { + "constant": { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "dst", - "sort": "int" - } - ] + "expression": { + "type": "int", + "var": "dst" + }, + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" } } } @@ -3602,53 +4488,96 @@ { "location": { "item": { - "var": "Token.name" + "contract": "Token", + "kind": "SVar", + "svar": "name" }, - "sort": "bytestring" + "type": "bytestring" }, - "value": "_name" + "value": { + "type": "bytestring", + "var": "_name" + } }, { "location": { "item": { - "var": "Token.symbol" + "contract": "Token", + "kind": "SVar", + "svar": "symbol" }, - "sort": "bytestring" + "type": "bytestring" }, - "value": "_symbol" + "value": { + "type": "bytestring", + "var": "_symbol" + } }, { "location": { "item": { - "var": "Token.totalSupply" + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" }, - "sort": "int" + "type": "int" }, - "value": "_totalSupply" + "value": { + "type": "int", + "var": "_totalSupply" + } }, { "location": { "item": { - "args": [ + "indexes": [ { - "var": "Token.balanceOf" - }, - [ - { - "expression": "Caller", - "sort": "int" - } - ] + "expression": "Caller", + "kind": "TypedExpr", + "sort": "int" + } ], - "arity": 2, - "symbol": "lookup" + "kind": "Mapping", + "reference": { + "contract": "Token", + "kind": "SVar", + "svar": "balanceOf" + } }, - "sort": "int" + "type": "int" }, - "value": "_totalSupply" + "value": { + "type": "int", + "var": "_totalSupply" + } } ], - "interface": "Token(string _symbol, string _name, string _version, uint256 _totalSupply)", + "interface": { + "args": [ + { + "abitype": "string", + "id": "\"_symbol\"", + "kind": "Declaration" + }, + { + "abitype": "string", + "id": "\"_name\"", + "kind": "Declaration" + }, + { + "abitype": "string", + "id": "\"_version\"", + "kind": "Declaration" + }, + { + "abitype": "uint256", + "id": "\"_totalSupply\"", + "kind": "Declaration" + } + ], + "id": "\"Token\"", + "kind": "Interface" + }, "invariants": [ { "contract": "Token", @@ -3658,15 +4587,24 @@ "args": [ { "args": [ - "0", - "_totalSupply" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "_totalSupply" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "_totalSupply", + { + "type": "int", + "var": "_totalSupply" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -3681,14 +4619,20 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "Token.totalSupply" + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, - "_totalSupply" + { + "type": "int", + "var": "_totalSupply" + } ], "arity": 2, "symbol": "==" @@ -3696,14 +4640,20 @@ { "args": [ { - "Post": { + "entry": { "item": { - "var": "Token.totalSupply" + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Post" }, - "_totalSupply" + { + "type": "int", + "var": "_totalSupply" + } ], "arity": 2, "symbol": "==" @@ -3714,14 +4664,20 @@ "args": [ { "args": [ - "0", { - "Pre": { + "literal": "0", + "type": "int" + }, + { + "entry": { "item": { - "var": "Token.totalSupply" + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" } ], "arity": 2, @@ -3730,12 +4686,15 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "Token.totalSupply" + "contract": "Token", + "kind": "SVar", + "svar": "totalSupply" }, - "sort": "int" - } + "type": "int" + }, + "timing": "Pre" }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], @@ -3756,15 +4715,24 @@ "args": [ { "args": [ - "0", - "_totalSupply" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "_totalSupply" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "_totalSupply", + { + "type": "int", + "var": "_totalSupply" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -3779,14 +4747,20 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "Token.name" + "contract": "Token", + "kind": "SVar", + "svar": "name" }, - "sort": "bytestring" - } + "type": "bytestring" + }, + "timing": "Pre" }, - "_name" + { + "type": "bytestring", + "var": "_name" + } ], "arity": 2, "symbol": "==" @@ -3794,14 +4768,20 @@ { "args": [ { - "Post": { + "entry": { "item": { - "var": "Token.name" + "contract": "Token", + "kind": "SVar", + "svar": "name" }, - "sort": "bytestring" - } + "type": "bytestring" + }, + "timing": "Post" }, - "_name" + { + "type": "bytestring", + "var": "_name" + } ], "arity": 2, "symbol": "==" @@ -3817,15 +4797,24 @@ "args": [ { "args": [ - "0", - "_totalSupply" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "_totalSupply" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "_totalSupply", + { + "type": "int", + "var": "_totalSupply" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -3840,14 +4829,20 @@ { "args": [ { - "Pre": { + "entry": { "item": { - "var": "Token.symbol" + "contract": "Token", + "kind": "SVar", + "svar": "symbol" }, - "sort": "bytestring" - } + "type": "bytestring" + }, + "timing": "Pre" }, - "_symbol" + { + "type": "bytestring", + "var": "_symbol" + } ], "arity": 2, "symbol": "==" @@ -3855,14 +4850,20 @@ { "args": [ { - "Post": { + "entry": { "item": { - "var": "Token.symbol" + "contract": "Token", + "kind": "SVar", + "svar": "symbol" }, - "sort": "bytestring" - } + "type": "bytestring" + }, + "timing": "Post" }, - "_symbol" + { + "type": "bytestring", + "var": "_symbol" + } ], "arity": 2, "symbol": "==" @@ -3878,15 +4879,24 @@ "args": [ { "args": [ - "0", - "_totalSupply" + { + "literal": "0", + "type": "int" + }, + { + "type": "int", + "var": "_totalSupply" + } ], "arity": 2, "symbol": "<=" }, { "args": [ - "_totalSupply", + { + "type": "int", + "var": "_totalSupply" + }, "115792089237316195423570985008687907853269984665640564039457584007913129639935" ], "arity": 2, @@ -3900,7 +4910,10 @@ "args": [ { "args": [ - "0", + { + "literal": "0", + "type": "int" + }, "Caller" ], "arity": 2, @@ -3923,7 +4936,7 @@ "kind": "Contract" } ], - "kind": "Program", + "kind": "Act", "store": { "kind": "Storages", "storages": { From 34d4c85b8fc894ffc8e77a1f9a8c2a76b298cac3 Mon Sep 17 00:00:00 2001 From: Zoe Paraskevopoulou Date: Wed, 11 Oct 2023 12:45:50 +0300 Subject: [PATCH 3/6] Update src/Syntax/TimeAgnostic.hs Co-authored-by: sophierain <99733455+sophierain@users.noreply.github.com> --- src/Syntax/TimeAgnostic.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Syntax/TimeAgnostic.hs b/src/Syntax/TimeAgnostic.hs index 5db4c762..5f7d89bf 100644 --- a/src/Syntax/TimeAgnostic.hs +++ b/src/Syntax/TimeAgnostic.hs @@ -462,7 +462,7 @@ field a c x = object [ "kind" .= pack "Field" instance ToJSON (TypedExp t) where toJSON (TExp typ a) = object [ "kind" .= pack "TypedExpr" - , "sort" .= pack (show typ) + , "type" .= pack (show typ) , "expression" .= toJSON a ] instance ToJSON (Exp a t) where From c8428f1be61cef682909d0cbb47a128a9e9ebb1a Mon Sep 17 00:00:00 2001 From: zoep Date: Wed, 11 Oct 2023 13:04:16 +0300 Subject: [PATCH 4/6] tests: regenerate tests output --- .../pass/safemath/safemathraw.act.typed.json | 2 +- .../frontend/pass/smoke/smoke.act.typed.json | 2 +- .../pass/token/transfer.act.typed.json | 226 +++++++++--------- 3 files changed, 115 insertions(+), 115 deletions(-) diff --git a/tests/frontend/pass/safemath/safemathraw.act.typed.json b/tests/frontend/pass/safemath/safemathraw.act.typed.json index 07364294..97bdcb4b 100644 --- a/tests/frontend/pass/safemath/safemathraw.act.typed.json +++ b/tests/frontend/pass/safemath/safemathraw.act.typed.json @@ -188,7 +188,7 @@ "symbol": "+" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, "stateUpdates": [] } diff --git a/tests/frontend/pass/smoke/smoke.act.typed.json b/tests/frontend/pass/smoke/smoke.act.typed.json index c7a534b8..bf4aaad5 100644 --- a/tests/frontend/pass/smoke/smoke.act.typed.json +++ b/tests/frontend/pass/smoke/smoke.act.typed.json @@ -63,7 +63,7 @@ "type": "int" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, "stateUpdates": [] } diff --git a/tests/frontend/pass/token/transfer.act.typed.json b/tests/frontend/pass/token/transfer.act.typed.json index 02345498..e0998847 100644 --- a/tests/frontend/pass/token/transfer.act.typed.json +++ b/tests/frontend/pass/token/transfer.act.typed.json @@ -61,7 +61,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -106,7 +106,7 @@ "var": "to" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -227,7 +227,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -254,7 +254,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -295,7 +295,7 @@ "var": "to" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -325,7 +325,7 @@ "var": "to" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -405,7 +405,7 @@ "type": "int" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, "stateUpdates": [ { @@ -416,7 +416,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -437,7 +437,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -472,7 +472,7 @@ "var": "to" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -496,7 +496,7 @@ "var": "to" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -581,7 +581,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -626,7 +626,7 @@ "var": "to" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -747,7 +747,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -774,7 +774,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -815,7 +815,7 @@ "var": "to" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -845,7 +845,7 @@ "var": "to" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -925,7 +925,7 @@ "type": "int" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, "stateUpdates": [ { @@ -936,7 +936,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -961,7 +961,7 @@ "var": "to" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1050,7 +1050,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1098,7 +1098,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1173,12 +1173,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1327,7 +1327,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1354,7 +1354,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1395,12 +1395,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1430,12 +1430,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1476,7 +1476,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1506,7 +1506,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1547,7 +1547,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1577,7 +1577,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1657,7 +1657,7 @@ "type": "int" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, "stateUpdates": [ { @@ -1668,7 +1668,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1693,12 +1693,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1723,7 +1723,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1747,7 +1747,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1782,7 +1782,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1806,7 +1806,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1879,12 +1879,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -1970,7 +1970,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2018,7 +2018,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2093,12 +2093,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2247,7 +2247,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2274,7 +2274,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2315,12 +2315,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2350,12 +2350,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2396,7 +2396,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2426,7 +2426,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2467,7 +2467,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2497,7 +2497,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2577,7 +2577,7 @@ "type": "int" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, "stateUpdates": [ { @@ -2588,7 +2588,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2613,12 +2613,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2643,7 +2643,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2667,7 +2667,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2702,7 +2702,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2726,7 +2726,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2799,12 +2799,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2890,7 +2890,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -2938,7 +2938,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3013,12 +3013,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3167,7 +3167,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3194,7 +3194,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3235,12 +3235,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3270,12 +3270,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3316,7 +3316,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3346,7 +3346,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3387,7 +3387,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3417,7 +3417,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3497,7 +3497,7 @@ "type": "int" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, "stateUpdates": [ { @@ -3508,7 +3508,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3533,12 +3533,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3562,12 +3562,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3602,7 +3602,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3626,7 +3626,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3661,7 +3661,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3685,7 +3685,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3767,7 +3767,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3815,7 +3815,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -3890,12 +3890,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -4044,7 +4044,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -4071,7 +4071,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -4112,12 +4112,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -4147,12 +4147,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -4193,7 +4193,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -4223,7 +4223,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -4264,7 +4264,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -4294,7 +4294,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -4374,7 +4374,7 @@ "type": "int" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, "stateUpdates": [ { @@ -4385,7 +4385,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -4410,12 +4410,12 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" }, { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -4440,7 +4440,7 @@ "var": "src" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -4465,7 +4465,7 @@ "var": "dst" }, "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", @@ -4534,7 +4534,7 @@ { "expression": "Caller", "kind": "TypedExpr", - "sort": "int" + "type": "int" } ], "kind": "Mapping", From 548ddc793b4135aa90fc15cbcefdfefe9db81107 Mon Sep 17 00:00:00 2001 From: zoep Date: Wed, 11 Oct 2023 14:37:13 +0300 Subject: [PATCH 5/6] add JSON for storage and AbiType --- src/Syntax/Untyped.hs | 45 +++++++++++++++++++++++++++++++++++++------ 1 file changed, 39 insertions(+), 6 deletions(-) diff --git a/src/Syntax/Untyped.hs b/src/Syntax/Untyped.hs index 1b10feee..9c15bd45 100644 --- a/src/Syntax/Untyped.hs +++ b/src/Syntax/Untyped.hs @@ -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 @@ -154,6 +155,7 @@ instance Show SlotType where <> ")") (show t) s + data StorageVar = StorageVar Pn SlotType Id deriving (Eq, Show) @@ -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 From d3b1b626cf55eb603e07e0b07d7ad00eee62f903 Mon Sep 17 00:00:00 2001 From: zoep Date: Wed, 11 Oct 2023 15:53:18 +0300 Subject: [PATCH 6/6] tests: regenerate tests output --- tests/frontend/pass/case/case.act.typed.json | 9 ++- .../pass/creation/create.act.typed.json | 17 ++++- .../frontend/pass/multi/multi.act.typed.json | 24 ++++++- .../pass/token/transfer.act.typed.json | 69 ++++++++++++++++--- 4 files changed, 104 insertions(+), 15 deletions(-) diff --git a/tests/frontend/pass/case/case.act.typed.json b/tests/frontend/pass/case/case.act.typed.json index 80c5425d..0de11f7a 100644 --- a/tests/frontend/pass/case/case.act.typed.json +++ b/tests/frontend/pass/case/case.act.typed.json @@ -559,7 +559,14 @@ "C": { "x": [ { - "type": "uint256" + "kind": "ValueType", + "valueType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } }, 0 ] diff --git a/tests/frontend/pass/creation/create.act.typed.json b/tests/frontend/pass/creation/create.act.typed.json index 00bd0a7b..27902efa 100644 --- a/tests/frontend/pass/creation/create.act.typed.json +++ b/tests/frontend/pass/creation/create.act.typed.json @@ -77,13 +77,26 @@ "Modest": { "x": [ { - "type": "uint256" + "kind": "ValueType", + "valueType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } }, 0 ], "y": [ { - "type": "address" + "kind": "ValueType", + "valueType": { + "abiType": { + "type": "Address" + }, + "kind": "AbiType" + } }, 1 ] diff --git a/tests/frontend/pass/multi/multi.act.typed.json b/tests/frontend/pass/multi/multi.act.typed.json index d801319e..e1ae9788 100644 --- a/tests/frontend/pass/multi/multi.act.typed.json +++ b/tests/frontend/pass/multi/multi.act.typed.json @@ -496,7 +496,14 @@ "A": { "x": [ { - "type": "uint256" + "kind": "ValueType", + "valueType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } }, 0 ] @@ -504,13 +511,24 @@ "B": { "a": [ { - "type": "A" + "kind": "ValueType", + "valueType": { + "kind": "ContractType", + "name": "\"A\"" + } }, 1 ], "y": [ { - "type": "uint256" + "kind": "ValueType", + "valueType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } }, 0 ] diff --git a/tests/frontend/pass/token/transfer.act.typed.json b/tests/frontend/pass/token/transfer.act.typed.json index e0998847..e44696c2 100644 --- a/tests/frontend/pass/token/transfer.act.typed.json +++ b/tests/frontend/pass/token/transfer.act.typed.json @@ -4943,35 +4943,86 @@ "Token": { "allowance": [ { - "ixTypes": "[address,address]", - "type": "mapping", - "valType": "uint256" + "ixTypes": [ + { + "abiType": { + "type": "Address" + }, + "kind": "AbiType" + }, + { + "abiType": { + "type": "Address" + }, + "kind": "AbiType" + } + ], + "kind": "MappingType", + "resType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } }, 4 ], "balanceOf": [ { - "ixTypes": "[address]", - "type": "mapping", - "valType": "uint256" + "ixTypes": [ + { + "abiType": { + "type": "Address" + }, + "kind": "AbiType" + } + ], + "kind": "MappingType", + "resType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } }, 3 ], "name": [ { - "type": "string" + "kind": "ValueType", + "valueType": { + "abiType": { + "type": "String" + }, + "kind": "AbiType" + } }, 0 ], "symbol": [ { - "type": "string" + "kind": "ValueType", + "valueType": { + "abiType": { + "type": "String" + }, + "kind": "AbiType" + } }, 1 ], "totalSupply": [ { - "type": "uint256" + "kind": "ValueType", + "valueType": { + "abiType": { + "size": "256", + "type": "UInt" + }, + "kind": "AbiType" + } }, 2 ]