add regression test

esbmc · lucasccordeiro · Jan 22, 2024 · Jan 20, 2024 · Jan 20, 2024 · Jan 20, 2024
commit ffaff4d5f32bce92bd7220e0e15b7b4c169d281a
diff --git a/regression/esbmc-solidity/scope_1/contract.sol b/regression/esbmc-solidity/scope_1/contract.sol
@@ -0,0 +1,22 @@
+// // SPDX-License-Identifier: GPL-3.0
+pragma solidity ^0.8.0;
+
+// Creating a contract
+contract Base {
+    uint x;
+
+    constructor() {
+        x = 1;
+    }
+
+    function test() public {
+        uint x = 10;
+        {
+            x = 2;
+        }
+        {
+            uint x = 3;
+        }
+        assert(x == 2);
+    }
+}
diff --git a/regression/esbmc-solidity/scope_1/contract.solast b/regression/esbmc-solidity/scope_1/contract.solast
@@ -0,0 +1,5 @@
+JSON AST (compact format):
+
+
+======= contract.sol =======
+{"absolutePath":"contract.sol","exportedSymbols":{"Base":[36]},"id":37,"license":"GPL-3.0","nodeType":"SourceUnit","nodes":[{"id":1,"literals":["solidity","^","0.8",".0"],"nodeType":"PragmaDirective","src":"39:23:0"},{"abstract":false,"baseContracts":[],"canonicalName":"Base","contractDependencies":[],"contractKind":"contract","fullyImplemented":true,"id":36,"linearizedBaseContracts":[36],"name":"Base","nameLocation":"96:4:0","nodeType":"ContractDefinition","nodes":[{"constant":false,"id":3,"mutability":"mutable","name":"x","nameLocation":"112:1:0","nodeType":"VariableDeclaration","scope":36,"src":"107:6:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":2,"name":"uint","nodeType":"ElementaryTypeName","src":"107:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"internal"},{"body":{"id":10,"nodeType":"Block","src":"134:22:0","statements":[{"expression":{"id":8,"isConstant":false,"isLValue":false,"isPure":false,"lValueRequested":false,"leftHandSide":{"id":6,"name":"x","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":3,"src":"144:1:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"nodeType":"Assignment","operator":"=","rightHandSide":{"hexValue":"31","id":7,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"148:1:0","typeDescriptions":{"typeIdentifier":"t_rational_1_by_1","typeString":"int_const 1"},"value":"1"},"src":"144:5:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":9,"nodeType":"ExpressionStatement","src":"144:5:0"}]},"id":11,"implemented":true,"kind":"constructor","modifiers":[],"name":"","nameLocation":"-1:-1:-1","nodeType":"FunctionDefinition","parameters":{"id":4,"nodeType":"ParameterList","parameters":[],"src":"131:2:0"},"returnParameters":{"id":5,"nodeType":"ParameterList","parameters":[],"src":"134:0:0"},"scope":36,"src":"120:36:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"},{"body":{"id":34,"nodeType":"Block","src":"185:135:0","statements":[{"assignments":[15],"declarations":[{"constant":false,"id":15,"mutability":"mutable","name":"x","nameLocation":"200:1:0","nodeType":"VariableDeclaration","scope":34,"src":"195:6:0","stateVariable":false,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":14,"name":"uint","nodeType":"ElementaryTypeName","src":"195:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"internal"}],"id":17,"initialValue":{"hexValue":"3130","id":16,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"204:2:0","typeDescriptions":{"typeIdentifier":"t_rational_10_by_1","typeString":"int_const 10"},"value":"10"},"nodeType":"VariableDeclarationStatement","src":"195:11:0"},{"id":22,"nodeType":"Block","src":"216:30:0","statements":[{"expression":{"id":20,"isConstant":false,"isLValue":false,"isPure":false,"lValueRequested":false,"leftHandSide":{"id":18,"name":"x","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":15,"src":"230:1:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"nodeType":"Assignment","operator":"=","rightHandSide":{"hexValue":"32","id":19,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"234:1:0","typeDescriptions":{"typeIdentifier":"t_rational_2_by_1","typeString":"int_const 2"},"value":"2"},"src":"230:5:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":21,"nodeType":"ExpressionStatement","src":"230:5:0"}]},{"id":27,"nodeType":"Block","src":"255:35:0","statements":[{"assignments":[24],"declarations":[{"constant":false,"id":24,"mutability":"mutable","name":"x","nameLocation":"274:1:0","nodeType":"VariableDeclaration","scope":27,"src":"269:6:0","stateVariable":false,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":23,"name":"uint","nodeType":"ElementaryTypeName","src":"269:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"internal"}],"id":26,"initialValue":{"hexValue":"33","id":25,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"278:1:0","typeDescriptions":{"typeIdentifier":"t_rational_3_by_1","typeString":"int_const 3"},"value":"3"},"nodeType":"VariableDeclarationStatement","src":"269:10:0"}]},{"expression":{"arguments":[{"commonType":{"typeIdentifier":"t_uint256","typeString":"uint256"},"id":31,"isConstant":false,"isLValue":false,"isPure":false,"lValueRequested":false,"leftExpression":{"id":29,"name":"x","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":15,"src":"306:1:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"nodeType":"BinaryOperation","operator":"==","rightExpression":{"hexValue":"32","id":30,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"311:1:0","typeDescriptions":{"typeIdentifier":"t_rational_2_by_1","typeString":"int_const 2"},"value":"2"},"src":"306:6:0","typeDescriptions":{"typeIdentifier":"t_bool","typeString":"bool"}}],"expression":{"argumentTypes":[{"typeIdentifier":"t_bool","typeString":"bool"}],"id":28,"name":"assert","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":-3,"src":"299:6:0","typeDescriptions":{"typeIdentifier":"t_function_assert_pure$_t_bool_$returns$__$","typeString":"function (bool) pure"}},"id":32,"isConstant":false,"isLValue":false,"isPure":false,"kind":"functionCall","lValueRequested":false,"nameLocations":[],"names":[],"nodeType":"FunctionCall","src":"299:14:0","tryCall":false,"typeDescriptions":{"typeIdentifier":"t_tuple$__$","typeString":"tuple()"}},"id":33,"nodeType":"ExpressionStatement","src":"299:14:0"}]},"functionSelector":"f8a8fd6d","id":35,"implemented":true,"kind":"function","modifiers":[],"name":"test","nameLocation":"171:4:0","nodeType":"FunctionDefinition","parameters":{"id":12,"nodeType":"ParameterList","parameters":[],"src":"175:2:0"},"returnParameters":{"id":13,"nodeType":"ParameterList","parameters":[],"src":"185:0:0"},"scope":36,"src":"162:158:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":37,"src":"87:235:0","usedErrors":[]}],"src":"39:283:0"}
diff --git a/regression/esbmc-solidity/scope_1/test.desc b/regression/esbmc-solidity/scope_1/test.desc
@@ -0,0 +1,4 @@
+CORE
+contract.solast
+--sol contract.sol --contract Base --k-induction
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/esbmc-solidity/scope_2/contract.sol b/regression/esbmc-solidity/scope_2/contract.sol
@@ -0,0 +1,22 @@
+// // SPDX-License-Identifier: GPL-3.0
+pragma solidity ^0.8.0;
+
+// Creating a contract
+contract Base {
+    uint x;
+
+    constructor() {
+        x = 1;
+    }
+
+    function test() public {
+        uint x = 10;
+        {
+            x = 2;
+        }
+        {
+            uint x = 3;
+        }
+        assert(x == 10);
+    }
+}
diff --git a/regression/esbmc-solidity/scope_2/contract.solast b/regression/esbmc-solidity/scope_2/contract.solast
@@ -0,0 +1,5 @@
+JSON AST (compact format):
+
+
+======= contract.sol =======
+{"absolutePath":"contract.sol","exportedSymbols":{"Base":[36]},"id":37,"license":"GPL-3.0","nodeType":"SourceUnit","nodes":[{"id":1,"literals":["solidity","^","0.8",".0"],"nodeType":"PragmaDirective","src":"39:23:0"},{"abstract":false,"baseContracts":[],"canonicalName":"Base","contractDependencies":[],"contractKind":"contract","fullyImplemented":true,"id":36,"linearizedBaseContracts":[36],"name":"Base","nameLocation":"96:4:0","nodeType":"ContractDefinition","nodes":[{"constant":false,"id":3,"mutability":"mutable","name":"x","nameLocation":"112:1:0","nodeType":"VariableDeclaration","scope":36,"src":"107:6:0","stateVariable":true,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":2,"name":"uint","nodeType":"ElementaryTypeName","src":"107:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"internal"},{"body":{"id":10,"nodeType":"Block","src":"134:22:0","statements":[{"expression":{"id":8,"isConstant":false,"isLValue":false,"isPure":false,"lValueRequested":false,"leftHandSide":{"id":6,"name":"x","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":3,"src":"144:1:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"nodeType":"Assignment","operator":"=","rightHandSide":{"hexValue":"31","id":7,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"148:1:0","typeDescriptions":{"typeIdentifier":"t_rational_1_by_1","typeString":"int_const 1"},"value":"1"},"src":"144:5:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":9,"nodeType":"ExpressionStatement","src":"144:5:0"}]},"id":11,"implemented":true,"kind":"constructor","modifiers":[],"name":"","nameLocation":"-1:-1:-1","nodeType":"FunctionDefinition","parameters":{"id":4,"nodeType":"ParameterList","parameters":[],"src":"131:2:0"},"returnParameters":{"id":5,"nodeType":"ParameterList","parameters":[],"src":"134:0:0"},"scope":36,"src":"120:36:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"},{"body":{"id":34,"nodeType":"Block","src":"185:136:0","statements":[{"assignments":[15],"declarations":[{"constant":false,"id":15,"mutability":"mutable","name":"x","nameLocation":"200:1:0","nodeType":"VariableDeclaration","scope":34,"src":"195:6:0","stateVariable":false,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":14,"name":"uint","nodeType":"ElementaryTypeName","src":"195:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"internal"}],"id":17,"initialValue":{"hexValue":"3130","id":16,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"204:2:0","typeDescriptions":{"typeIdentifier":"t_rational_10_by_1","typeString":"int_const 10"},"value":"10"},"nodeType":"VariableDeclarationStatement","src":"195:11:0"},{"id":22,"nodeType":"Block","src":"216:30:0","statements":[{"expression":{"id":20,"isConstant":false,"isLValue":false,"isPure":false,"lValueRequested":false,"leftHandSide":{"id":18,"name":"x","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":15,"src":"230:1:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"nodeType":"Assignment","operator":"=","rightHandSide":{"hexValue":"32","id":19,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"234:1:0","typeDescriptions":{"typeIdentifier":"t_rational_2_by_1","typeString":"int_const 2"},"value":"2"},"src":"230:5:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"id":21,"nodeType":"ExpressionStatement","src":"230:5:0"}]},{"id":27,"nodeType":"Block","src":"255:35:0","statements":[{"assignments":[24],"declarations":[{"constant":false,"id":24,"mutability":"mutable","name":"x","nameLocation":"274:1:0","nodeType":"VariableDeclaration","scope":27,"src":"269:6:0","stateVariable":false,"storageLocation":"default","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"},"typeName":{"id":23,"name":"uint","nodeType":"ElementaryTypeName","src":"269:4:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"visibility":"internal"}],"id":26,"initialValue":{"hexValue":"33","id":25,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"278:1:0","typeDescriptions":{"typeIdentifier":"t_rational_3_by_1","typeString":"int_const 3"},"value":"3"},"nodeType":"VariableDeclarationStatement","src":"269:10:0"}]},{"expression":{"arguments":[{"commonType":{"typeIdentifier":"t_uint256","typeString":"uint256"},"id":31,"isConstant":false,"isLValue":false,"isPure":false,"lValueRequested":false,"leftExpression":{"id":29,"name":"x","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":15,"src":"306:1:0","typeDescriptions":{"typeIdentifier":"t_uint256","typeString":"uint256"}},"nodeType":"BinaryOperation","operator":"==","rightExpression":{"hexValue":"3130","id":30,"isConstant":false,"isLValue":false,"isPure":true,"kind":"number","lValueRequested":false,"nodeType":"Literal","src":"311:2:0","typeDescriptions":{"typeIdentifier":"t_rational_10_by_1","typeString":"int_const 10"},"value":"10"},"src":"306:7:0","typeDescriptions":{"typeIdentifier":"t_bool","typeString":"bool"}}],"expression":{"argumentTypes":[{"typeIdentifier":"t_bool","typeString":"bool"}],"id":28,"name":"assert","nodeType":"Identifier","overloadedDeclarations":[],"referencedDeclaration":-3,"src":"299:6:0","typeDescriptions":{"typeIdentifier":"t_function_assert_pure$_t_bool_$returns$__$","typeString":"function (bool) pure"}},"id":32,"isConstant":false,"isLValue":false,"isPure":false,"kind":"functionCall","lValueRequested":false,"nameLocations":[],"names":[],"nodeType":"FunctionCall","src":"299:15:0","tryCall":false,"typeDescriptions":{"typeIdentifier":"t_tuple$__$","typeString":"tuple()"}},"id":33,"nodeType":"ExpressionStatement","src":"299:15:0"}]},"functionSelector":"f8a8fd6d","id":35,"implemented":true,"kind":"function","modifiers":[],"name":"test","nameLocation":"171:4:0","nodeType":"FunctionDefinition","parameters":{"id":12,"nodeType":"ParameterList","parameters":[],"src":"175:2:0"},"returnParameters":{"id":13,"nodeType":"ParameterList","parameters":[],"src":"185:0:0"},"scope":36,"src":"162:159:0","stateMutability":"nonpayable","virtual":false,"visibility":"public"}],"scope":37,"src":"87:236:0","usedErrors":[]}],"src":"39:284:0"}
diff --git a/regression/esbmc-solidity/scope_2/test.desc b/regression/esbmc-solidity/scope_2/test.desc
@@ -0,0 +1,4 @@
+CORE
+contract.solast
+--sol contract.sol --contract Base --k-induction
+^VERIFICATION FAILED$
diff --git a/regression/esbmc-solidity/scope_3/contract.sol b/regression/esbmc-solidity/scope_3/contract.sol
@@ -0,0 +1,21 @@
+// // SPDX-License-Identifier: GPL-3.0
+pragma solidity ^0.8.0;
+
+// Creating a contract
+contract Base {
+    uint x;
+
+    constructor() {
+        x = 1;
+    }
+
+    function test() public {
+        {
+            x = 2;
+        }
+        {
+            uint x = 3;
+        }
+        assert(x == 1);
+    }
+}