Regression: Constructor call

regression/constructor_call/Makefile

@@ -0,0 +1,135 @@
+MAKEFLAGS = --no-print-directory
+
+# CHANGE THIS PATHS
+# Original contract path
+CONTRACT = ./versions/
+# Contract with solcmc instrumentation path
+SOLCMC_CONTRACT = ./solcmc/generated
+# Certora specifications path
+CERTORA_SPEC = ./certora
+
+SKELETON = ./skeleton.json
+GROUND_TRUTH = ./ground-truth.csv
+README = ./README.md
+BUILD_DIR = ./build
+
+# SOLCMC params
+to = 10m
+Z3_DIR = $(BUILD_DIR)/z3
+Z3_OUT = $(Z3_DIR)/out.csv
+Z3_CM = $(Z3_DIR)/cm.csv
+Z3_TABLE = $(Z3_DIR)/table.md
+Z3_LOGS = $(Z3_DIR)/logs
+ELD_DIR = $(BUILD_DIR)/eld
+ELD_OUT = $(ELD_DIR)/out.csv
+ELD_CM = $(ELD_DIR)/cm.csv
+ELD_TABLE = $(ELD_DIR)/table.md
+ELD_LOGS = $(ELD_DIR)/logs
+
+# Certora params
+CERTORA_DIR = $(BUILD_DIR)/certora
+CERTORA_OUT = $(CERTORA_DIR)/out.csv
+CERTORA_CM = $(CERTORA_DIR)/cm.csv
+CERTORA_TABLE = $(CERTORA_DIR)/table.md
+CERTORA_LOGS = $(CERTORA_DIR)/logs
+
+PYTHON = python3
+
+.PHONY: all certora solcmc solcmc-contracts plain clean cleanr
+
+all: plain solcmc certora
+	@echo "Adding Solcmc table to README..."
+	@echo "### SolCMC" >> $(README)
+	@cat $(Z3_TABLE) >> $(README)
+	@cat $(ELD_TABLE) >> $(README)
+	@echo "" >> $(README)
+	@echo "Adding Certora table to README..."
+	@cat $(CERTORA_TABLE) >> $(README)
+
+#---------------------------- CERTORA ----------------------------#
+certora: $(CERTORA_TABLE)
+
+$(CERTORA_TABLE): $(CERTORA_CM)
+	@echo "Generating Certora results table ($(CERTORA_TABLE))..."
+	@echo "### Certora" > $(CERTORA_TABLE)
+	@$(PYTHON) ../../scripts/mdtable_gen.py --input $(CERTORA_CM) >> $(CERTORA_TABLE)
+
+$(CERTORA_CM): $(GROUND_TRUTH) $(CERTORA_OUT) 
+	@echo "Generating Certora confusion matrix ($(CERTORA_CM))..."
+	@$(PYTHON) ../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(CERTORA_OUT) > $(CERTORA_CM)
+
+$(CERTORA_OUT): setup
+	@echo "Running Certora experiments..."
+	@$(PYTHON) ../../scripts/run_certora.py --contracts $(CONTRACT) --specs $(CERTORA_SPEC) --output $(CERTORA_DIR)
+
+#---------------------------- SOLCMC -----------------------------#
+solcmc: solcmc-contracts $(Z3_TABLE) $(ELD_TABLE)
+
+solcmc-contracts:
+	$(MAKE) -C solcmc build
+
+# Solcmc with Z3
+# Make markdown table
+$(Z3_TABLE): $(Z3_CM)
+	@echo "Generating SolCMC results table ($(Z3_TABLE))..."
+	echo "#### Z3" > $(Z3_TABLE)
+	@$(PYTHON) ../../scripts/mdtable_gen.py --input $(Z3_CM) >> $(Z3_TABLE)
+
+# Build confusion matrix with ground truths
+$(Z3_CM): $(GROUND_TRUTH) $(Z3_OUT)
+	@echo "Generating Solcmc confusion matrix ($(Z3_CM))..."
+	@$(PYTHON) ../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(Z3_OUT) > $(Z3_CM)
+
+# Run experiments
+$(Z3_OUT): setup
+	@echo "Running SolCMC ($(solver)) experiments..."
+	@$(PYTHON) ../../scripts/run_solcmc.py --contracts $(SOLCMC_CONTRACT) --output $(Z3_DIR) --timeout $(to) --solver z3
+
+# Solcmc with eldarica
+# Make markdown table
+$(ELD_TABLE): $(ELD_CM)
+	@echo "Generating SolCMC results table ($(ELD_TABLE))..."
+	echo "#### ELD" > $(ELD_TABLE)
+	@$(PYTHON) ../../scripts/mdtable_gen.py --input $(ELD_CM) >> $(ELD_TABLE)
+
+# Build confusion matrix with ground truths
+$(ELD_CM): $(GROUND_TRUTH) $(ELD_OUT)
+	@echo "Generating Solcmc confusion matrix ($(ELD_CM))..."
+	@$(PYTHON) ../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(ELD_OUT) > $(ELD_CM)
+
+# Run experiments
+$(ELD_OUT): setup
+	@echo "Running SolCMC ($(solver)) experiments..."
+	@$(PYTHON) ../../scripts/run_solcmc.py --contracts $(SOLCMC_CONTRACT) --output $(ELD_DIR) --timeout $(to) --solver eld
+
+#---------------------------- SETUP ------------------------------#
+setup: $(Z3_LOGS) $(ELD_LOGS) $(CERTORA_LOGS)
+
+# Create build logs/ dirs, and build/ dirs with them
+$(Z3_LOGS):
+	@mkdir -p $@
+
+$(ELD_LOGS):
+	@mkdir -p $@
+
+$(CERTORA_LOGS):
+	@mkdir -p $@
+
+#---------------------------- README -----------------------------#
+plain: cleanr $(README)
+
+# Create plain README, without experiments results
+$(README): $(VERSIONS_DIR) $(SKELETON) $(GROUND_TRUTH)
+	@echo "Generating plain README..."
+	@$(PYTHON) ../../scripts/readme_gen.py -d . > $(README)
+	@echo "## Experiments" >> $(README)
+
+#---------------------------- CLEAN ------------------------------#
+clean: cleanr
+	@echo "Removing $(BUILD_DIR)..."
+	@rm -rf $(BUILD_DIR)
+
+# Remove README.md
+cleanr:
+	@echo "Removing README..."
+	@rm -f $(README)

regression/constructor_call/README.md

@@ -0,0 +1,58 @@
+# Constructor Call
+
+## Specification
+The `ConstructorCall` contract is designed to initialize and manage a list of values provided during contract deployment. It performs basic aggregation and storage operations on these values, ensuring certain constraints are met. Below are the key specifications:
+
+## **Initialization via Constructor**
+- The contract requires an array of unsigned integers (`uint256[]`) as input during deployment.
+- The length of the input array must match a predefined constant (`LENGHT`), which is set to **10**.
+- Each value in the array is validated to ensure it is **greater than zero** before being processed.
+
+
+## **Sum Calculation**
+- The contract maintains a private variable `sum` that aggregates the values provided during deployment.
+- The `doSum` function is used to:
+  - Add each value to the `sum`.
+  - Store the value in the `values` array.
+
+
+## **Storage of Values**
+- The contract stores all validated values in a private array `values`.
+- These values can be accessed indirectly through the `getSumOfValues` function.
+
+
+## **Getter Function for Aggregation**
+- The `getSumOfValues` function:
+  - Calculates and returns the sum of all values stored in the `values` array.
+  - Provides visibility into the aggregated data for verification purposes.
+
+## Properties
+- **sum-matches-array-values**: The sum calculated by the contract during the constructor matches the sum of the values in the array passed to it.
+
+## Ground truth
+|        | sum-matches-array-values |
+|--------|--------------------------|
+| **v1** | 1                        |
+
+
+## Experiments
+### SolCMC
+#### Z3
+|        | sum-matches-array-values |
+|--------|--------------------------|
+| **v1** | UNK                      |
+
+
+#### ELD
+|        | sum-matches-array-values |
+|--------|--------------------------|
+| **v1** | FN!                      |
+
+
+
+### Certora
+|        | sum-matches-array-values |
+|--------|--------------------------|
+| **v1** | FN                       |
+
+

regression/constructor_call/certora/conf/ConstructorCall_sum-matches-array-values_v1.conf

@@ -0,0 +1,7 @@
+{ 
+    "files": [
+        "ConstructorCall_v1.sol:ConstructorCall",
+    ],
+    "verify": "ConstructorCall:certora/sum-matches-array-values.spec",
+    "msg": "ConstructorCall_sum-matches-array-values_v1"
+}

regression/constructor_call/certora/sum-matches-array-values.spec

@@ -0,0 +1,5 @@
+rule sum_matches_array_values {
+    env e;
+
+    assert currentContract.sum == getSumOfValues(e);
+}

regression/constructor_call/ground-truth.csv

@@ -0,0 +1,2 @@
+property,version,truth,footnote-md
+sum-matches-array-values,v1,1,

regression/constructor_call/skeleton.json

@@ -0,0 +1,7 @@
+{
+    "name": "Constructor Call",
+    "specification": "file:specs.md",
+    "properties": {
+        "sum-matches-array-values": "The sum calculated by the contract during the constructor matches the sum of the values in the array passed to it."
+    }
+}

regression/constructor_call/solcmc/Makefile

@@ -0,0 +1,21 @@
+PYTHON          := python3
+VERSIONS_DIR    := ../versions
+PROPERTIES_DIR  := .
+CONTRACTS_DIR   := generated
+
+.PHONY: build clean
+.DEFAULT_GOAL := build
+
+$(CONTRACTS_DIR):
+	@mkdir -p $@
+
+build: clean $(CONTRACTS_DIR)
+	@echo "> running builder.py …"
+	@$(PYTHON) ../../../scripts/builder.py \
+	    --versions   $(VERSIONS_DIR) \
+	    --properties $(PROPERTIES_DIR) \
+	    --output     $(CONTRACTS_DIR)
+	@echo "files written to $(CONTRACTS_DIR)/"
+
+clean:
+	@rm -rf $(CONTRACTS_DIR)

regression/constructor_call/solcmc/generated/ConstructorCall_sum-matches-array-values_v1.sol

@@ -0,0 +1,42 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+contract ConstructorCall {
+    uint256 private sum;
+
+    //macro for length of values
+    uint256 private constant LENGHT = 3;
+
+    uint256[] private values;
+
+    constructor(uint256[] memory _values) {
+        require(_values.length == LENGHT);
+
+        for (uint256 i = 0; i < LENGHT; i++) {
+            require (_values[i] > 0, "Value must be greater than zero");
+            doSum(_values[i]);
+        }
+    }
+
+    function doSum(uint256 _value) public {
+        require(_value > 0); //double require
+
+        sum += _value;
+        values.push(_value);
+    }
+
+    function getSumOfValues() public view returns (uint256) {
+        uint256 total = 0;
+        for (uint256 i = 0; i < LENGHT; i++) {
+            total += values[i];
+        }
+        return total;
+    }
+    function invariant()public  view {
+        assert (sum == getSumOfValues());
+    }
+
+}
+
+

regression/constructor_call/solcmc/sum-matches-array-values.sol

@@ -0,0 +1,3 @@
+function invariant()public  view {
+    assert (sum == getSumOfValues());
+}

regression/constructor_call/specs.md

@@ -0,0 +1,24 @@
+The `ConstructorCall` contract is designed to initialize and manage a list of values provided during contract deployment. It performs basic aggregation and storage operations on these values, ensuring certain constraints are met. Below are the key specifications:
+
+## **Initialization via Constructor**
+- The contract requires an array of unsigned integers (`uint256[]`) as input during deployment.
+- The length of the input array must match a predefined constant (`LENGHT`), which is set to **10**.
+- Each value in the array is validated to ensure it is **greater than zero** before being processed.
+
+
+## **Sum Calculation**
+- The contract maintains a private variable `sum` that aggregates the values provided during deployment.
+- The `doSum` function is used to:
+  - Add each value to the `sum`.
+  - Store the value in the `values` array.
+
+
+## **Storage of Values**
+- The contract stores all validated values in a private array `values`.
+- These values can be accessed indirectly through the `getSumOfValues` function.
+
+
+## **Getter Function for Aggregation**
+- The `getSumOfValues` function:
+  - Calculates and returns the sum of all values stored in the `values` array.
+  - Provides visibility into the aggregated data for verification purposes.

regression/constructor_call/versions/ConstructorCall_v1.sol

@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+contract ConstructorCall {
+    uint256 private sum;
+
+    //macro for length of values
+    uint256 private constant LENGHT = 3;
+
+    uint256[] private values;
+
+    constructor(uint256[] memory _values) {
+        require(_values.length == LENGHT);
+
+        for (uint256 i = 0; i < LENGHT; i++) {
+            require (_values[i] > 0, "Value must be greater than zero");
+            doSum(_values[i]);
+        }
+    }
+
+    function doSum(uint256 _value) public {
+        require(_value > 0); //double require
+
+        sum += _value;
+        values.push(_value);
+    }
+
+    function getSumOfValues() public view returns (uint256) {
+        uint256 total = 0;
+        for (uint256 i = 0; i < LENGHT; i++) {
+            total += values[i];
+        }
+        return total;
+    }
+}
+
+