Regression: Added constructor and POC to external_abstract

regression/external_abstract/ExternalAbstract_v1.sol

@@ -8,14 +8,21 @@ abstract contract D {
 contract ExternalAbstract {
 	uint x;
 	D d;
+
+	constructor(D _d) {
+		d = _d;
+	}
+
 	function f() public {
 		if (x < 10)
 			++x;
 	}
+
 	function g() public {
 		require(x < 10);
 		d.d();
 	}
+
 	function getX() public view returns (uint) {
 		return x;
 	}

regression/external_abstract/README.md

@@ -51,7 +51,7 @@ We cannot trust `d.d` call because `d` could be implemented to call the function
 #### Z3
 |        | x-abstract-call |
 |--------|-----------------|
-| **v1** | TN!             |
+| **v1** | TN              |
 
 
 #### ELD

regression/external_abstract/hardhat/Makefile

@@ -0,0 +1,33 @@
+SHELL := /bin/bash
+
+.PHONY: init test clean 
+
+default: test
+
+init:
+	@if [ -f hardhat.config.js ]; then \
+		echo "Skipping: Hardhat already initialized."; \
+	else \
+		echo "Initializing Hardhat project..."; \
+		npm init -y >/dev/null && \
+		npm install --save-dev hardhat --silent --no-progress >/dev/null && \
+		printf '3\n' | npx hardhat init  && \
+		npm install --save-dev @nomicfoundation/hardhat-toolbox --silent --no-progress >/dev/null && \
+		if ! grep -q '@nomicfoundation/hardhat-toolbox' hardhat.config.js; then \
+			sed -i '1irequire("@nomicfoundation/hardhat-toolbox")\n' hardhat.config.js; \
+		fi; \
+		echo "Done."; \
+	fi
+
+test: init
+	npx hardhat test
+
+
+clean:
+	@echo "Cleaning project (preserving Makefile, contracts/, and test/)..."
+	@find . -mindepth 1 -maxdepth 1 \
+		! -name 'Makefile' \
+		! -name 'contracts' \
+		! -name 'test' \
+		-exec rm -rf {} +
+	@echo "Clean complete."

regression/external_abstract/hardhat/contracts/D_impl_v1.sol

@@ -0,0 +1,14 @@
+pragma solidity ^0.8.25;
+
+import "./ExternalAbstract_v1.sol";
+
+contract DImpl is D {
+    ExternalAbstract ext;
+    function d() external override {
+        ext.f();
+    }
+
+    function set_ext(ExternalAbstract e) public{
+        ext = e;
+    }
+}

regression/external_abstract/hardhat/contracts/ExternalAbstract_v1.sol

@@ -0,0 +1,29 @@
+//https://github.com/leonardoalt/cav_2022_artifact/blob/main/regression/external_calls/external.sol
+pragma solidity ^0.8.25;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract ExternalAbstract {
+	uint x;
+	D d;
+
+	constructor(D _d) {
+		d = _d;
+	}
+
+	function f() public {
+		if (x < 10)
+			++x;
+	}
+
+	function g() public {
+		require(x < 10);
+		d.d();
+	}
+
+	function getX() public view returns (uint) {
+		return x;
+	}
+}

regression/external_abstract/hardhat/test/test.js

@@ -0,0 +1,26 @@
+const {
+    loadFixture
+} = require("@nomicfoundation/hardhat-toolbox/network-helpers");
+const { expect } = require("chai");
+
+describe("ExternalAbstract", function () {
+    async function deployContract () {
+        const DImpl = await ethers.deployContract("DImpl");
+        const ExternalAbstract = await ethers.deployContract(
+            "ExternalAbstract", [ DImpl ]
+        );
+
+        await DImpl.set_ext(ExternalAbstract);
+
+        return { ExternalAbstract };
+    }
+
+    it("If an implementation of `D` which calls `f()` is used in the contract, when `g()` is called the value of `x` will change", async function () {
+        const { ExternalAbstract } = await loadFixture(deployContract);
+
+        const x_before = await ExternalAbstract.getX();
+        await ExternalAbstract.g();
+
+        expect(await ExternalAbstract.getX()).to.not.equal(x_before);
+    })
+})

regression/external_abstract/solcmc/ExternalAbstract_x-abstract-call_v1.sol

@@ -8,13 +8,23 @@ abstract contract D {
 contract ExternalAbstract {
 	uint x;
 	D d;
+
+	constructor(D _d) {
+		d = _d;
+	}
+
 	function f() public {
 		if (x < 10)
 			++x;
 	}
+
 	function g() public {
 		require(x < 10);
 		d.d();
 		assert(x < 10);
 	}
+
+	function getX() public view returns (uint) {
+		return x;
+	}
 }