From eb356735f66a0ed9504537f675197a8d2647bdb5 Mon Sep 17 00:00:00 2001
From: Martin Blicha <blichm@usi.ch>
Date: Mon, 7 Dec 2020 11:03:07 +0100
Subject: [PATCH] [SMTChecker] Adding support for reporting values of structs
 in CEX in CHC engine.

---
 Changelog.md                     |  1 +
 libsolidity/formal/Predicate.cpp | 33 +++++++++++++++++++++++++++++++-
 2 files changed, 33 insertions(+), 1 deletion(-)

diff --git a/Changelog.md b/Changelog.md
index 5a1cfa9bf..a8dff3f86 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -12,6 +12,7 @@ Compiler Features:
  * SMTChecker: Support struct constructor.
  * SMTChecker: Support getters.
  * SMTChecker: Support early returns in the CHC engine.
+ * SMTChecker: Report struct values in counterexamples from CHC engine.
  * Standard-Json: Properly filter the requested output artifacts.
 
 Bugfixes:
diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp
index 335cabb98..b95738eaf 100644
--- a/libsolidity/formal/Predicate.cpp
+++ b/libsolidity/formal/Predicate.cpp
@@ -302,7 +302,15 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
 		auto const& tupleSort = dynamic_cast<TupleSort const&>(*_expr.sort);
 		solAssert(tupleSort.components.size() == 2, "");
 
-		auto length = stoul(_expr.arguments.at(1).name);
+		unsigned long length;
+		try
+		{
+			length = stoul(_expr.arguments.at(1).name);
+		}
+		catch(out_of_range const&)
+		{
+			return {};
+		}
 		// Limit this counterexample size to 1k.
 		// Some OSs give you "unlimited" memory through swap and other virtual memory,
 		// so purely relying on bad_alloc being thrown is not a good idea.
@@ -321,6 +329,22 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
 			// Solver gave a concrete array but length is too large.
 		}
 	}
+	if (smt::isNonRecursiveStruct(*_type))
+	{
+		auto const& structType = dynamic_cast<StructType const&>(*_type);
+		solAssert(_expr.name == "tuple_constructor", "");
+		auto const& tupleSort = dynamic_cast<TupleSort const&>(*_expr.sort);
+		auto members = structType.structDefinition().members();
+		solAssert(tupleSort.components.size() == members.size(), "");
+		solAssert(_expr.arguments.size() == members.size(), "");
+		vector<string> elements;
+		for (unsigned i = 0; i < members.size(); ++i)
+		{
+			optional<string> elementStr = expressionToString(_expr.arguments.at(i), members[i]->type());
+			elements.push_back(members[i]->name() + (elementStr.has_value() ?  ": " + elementStr.value() : ""));
+		}
+		return "{" + boost::algorithm::join(elements, ", ") + "}";
+	}
 
 	return {};
 }
@@ -366,5 +390,12 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _arr
 		return true;
 	}
 
+	// Special base case, not supported yet.
+	if (_expr.name.rfind("(_ as-array") == 0)
+	{
+		// Z3 expression representing reinterpretation of a different term as an array
+		return false;
+	}
+
 	solAssert(false, "");
 }