From cf35785328b477343b7c1b135b91c328cb220fce Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Mon, 19 Oct 2020 18:11:59 +0100
Subject: [PATCH] Add unknown message to all verification targets

---
 Changelog.md                                    |  4 ++++
 libsolidity/formal/CHC.cpp                      | 17 ++++++++++-------
 .../crypto/crypto_functions_fail.sol            |  3 +++
 ...s_same_input_over_state_same_output_fail.sol |  3 +++
 .../smtCheckerTests/imports/import_base.sol     |  1 +
 .../invariants/loop_nested_for.sol              |  1 +
 .../smtCheckerTests/loops/for_1_fail.sol        |  1 +
 .../loops/for_1_false_positive.sol              |  1 +
 ...hile_loop_array_assignment_memory_memory.sol |  1 +
 ...ile_loop_array_assignment_memory_storage.sol |  1 +
 ...le_loop_array_assignment_storage_storage.sol |  1 +
 .../operators/compound_bitwise_or_int_1.sol     |  1 +
 .../operators/compound_bitwise_or_uint_1.sol    |  1 +
 .../operators/compound_bitwise_or_uint_2.sol    |  1 +
 .../operators/compound_bitwise_or_uint_3.sol    |  1 +
 .../smtCheckerTests/operators/mod_signed.sol    |  1 +
 .../operators/slice_default_end.sol             |  3 +++
 .../operators/slice_default_start.sol           |  1 +
 18 files changed, 36 insertions(+), 7 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index cd3806d18..170b7d46e 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,6 +1,10 @@
 ### 0.7.5 (unreleased)
 
 
+Bugfixes:
+ * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine.
+
+
 
 ### 0.7.4 (2020-10-19)
 
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index ea14bf12e..880e9c553 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -1215,22 +1215,25 @@ void CHC::checkVerificationTargets()
 				if (!intType)
 					intType = TypeProvider::uint256();
 
-				satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ") happens here.";
-				satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ") happens here.";
+				satMsgUnderflow = "Underflow (resulting value less than " + formatNumberReadable(intType->minValue()) + ")";
+				satMsgOverflow = "Overflow (resulting value larger than " + formatNumberReadable(intType->maxValue()) + ")";
 				if (target.type == VerificationTarget::Type::Underflow)
 				{
-					satMsg = satMsgUnderflow;
+					satMsg = satMsgUnderflow + " happens here.";
+					unknownMsg = satMsgUnderflow + " might happen here.";
 					errorReporterId = underflowErrorId;
 				}
 				else if (target.type == VerificationTarget::Type::Overflow)
 				{
-					satMsg = satMsgOverflow;
+					satMsg = satMsgOverflow + " happens here.";
+					unknownMsg = satMsgOverflow + " might happen here.";
 					errorReporterId = overflowErrorId;
 				}
 			}
 			else if (target.type == VerificationTarget::Type::DivByZero)
 			{
 				satMsg = "Division by zero happens here.";
+				unknownMsg = "Division by zero might happen here.";
 				errorReporterId = 4281_error;
 			}
 			else
@@ -1246,12 +1249,12 @@ void CHC::checkVerificationTargets()
 			{
 				auto specificTarget = target;
 				specificTarget.type = VerificationTarget::Type::Underflow;
-				checkAndReportTarget(scope, specificTarget, errorId, underflowErrorId, satMsgUnderflow, unknownMsg);
+				checkAndReportTarget(scope, specificTarget, errorId, underflowErrorId, satMsgUnderflow + " happens here.", satMsgUnderflow + " might happen here.");
 
 				++it;
 				solAssert(it != m_errorIds.end(), "");
 				specificTarget.type = VerificationTarget::Type::Overflow;
-				checkAndReportTarget(scope, specificTarget, it->second, overflowErrorId, satMsgOverflow, unknownMsg);
+				checkAndReportTarget(scope, specificTarget, it->second, overflowErrorId, satMsgOverflow + " happens here.", satMsgOverflow + " might happen here.");
 			}
 		}
 	}
@@ -1267,7 +1270,7 @@ void CHC::checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const&
 		solAssert(it != m_errorIds.end(), "");
 		unsigned errorId = it->second;
 
-		checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here.");
+		checkAndReportTarget(assertion, _target, errorId, 6328_error, "Assertion violation happens here.", "Assertion violation might happen here.");
 	}
 }
 
diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
index 5f9a7f22e..36e34cc4d 100644
--- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
+++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
@@ -24,8 +24,11 @@ contract C {
 }
 // ----
 // Warning 1218: (168-184): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (168-184): CHC: Assertion violation might happen here.
 // Warning 1218: (305-321): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (305-321): CHC: Assertion violation might happen here.
 // Warning 1218: (448-464): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (448-464): CHC: Assertion violation might happen here.
 // Warning 6328: (673-689): CHC: Assertion violation happens here.
 // Warning 4661: (168-184): BMC: Assertion violation happens here.
 // Warning 4661: (305-321): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
index 9d8c98479..10c6ada8e 100644
--- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
+++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
@@ -46,8 +46,11 @@ contract C {
 }
 // ----
 // Warning 1218: (726-745): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (726-745): CHC: Assertion violation might happen here.
 // Warning 1218: (749-768): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (749-768): CHC: Assertion violation might happen here.
 // Warning 1218: (772-791): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (772-791): CHC: Assertion violation might happen here.
 // Warning 6328: (795-814): CHC: Assertion violation happens here.
 // Warning 4661: (726-745): BMC: Assertion violation happens here.
 // Warning 4661: (749-768): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/imports/import_base.sol b/test/libsolidity/smtCheckerTests/imports/import_base.sol
index eca0249c2..e7bf269be 100644
--- a/test/libsolidity/smtCheckerTests/imports/import_base.sol
+++ b/test/libsolidity/smtCheckerTests/imports/import_base.sol
@@ -18,6 +18,7 @@ contract Der is Base {
 	}
 }
 // ----
+// Warning 4984: (der:101-109): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 6328: (der:113-126): CHC: Assertion violation happens here.
 // Warning 2661: (base:100-103): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (der:101-109): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol b/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol
index 8365c0e4b..1b971795a 100644
--- a/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol
+++ b/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol
@@ -13,4 +13,5 @@ contract Simple {
 	}
 }
 // ----
+// Warning 6328: (187-201): CHC: Assertion violation might happen here.
 // Warning 4661: (187-201): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
index c05da9572..1135d12e7 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_1_fail.sol
@@ -14,5 +14,6 @@ contract C
 // ====
 // SMTSolvers: z3
 // ----
+// Warning 4984: (176-181): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 6328: (189-203): CHC: Assertion violation happens here.
 // Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
index f4176588e..29afb548f 100644
--- a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
+++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
@@ -14,4 +14,5 @@ contract C
 	}
 }
 // ----
+// Warning 4984: (176-181): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
index d540351a2..41d602961 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
@@ -20,5 +20,6 @@ contract LoopFor2 {
 // ====
 // SMTSolvers: z3
 // ----
+// Warning 4984: (244-249): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 6328: (373-392): CHC: Assertion violation happens here.
 // Warning 6328: (396-415): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
index 50a91d19b..29509fc5c 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
@@ -25,3 +25,4 @@ contract LoopFor2 {
 // ====
 // SMTSolvers: z3
 // ----
+// Warning 4984: (237-242): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
index 6bf40282a..44a94090b 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
@@ -20,5 +20,6 @@ contract LoopFor2 {
 	}
 }
 // ----
+// Warning 4984: (229-234): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 6328: (290-309): CHC: Assertion violation happens here.
 // Warning 6328: (313-332): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
index e25ae354d..7c198b24e 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol
@@ -9,3 +9,4 @@ contract C {
     }
 }
 // ----
+// Warning 6328: (174-212): CHC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol
index 790d30a76..7a3441661 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol
@@ -9,3 +9,4 @@ contract C {
     }
 }
 // ----
+// Warning 6328: (166-183): CHC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
index 714c0df22..6e62d8148 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
@@ -11,4 +11,5 @@ contract C {
     }
 }
 // ----
+// Warning 6328: (173-192): CHC: Assertion violation might happen here.
 // Warning 7812: (173-192): BMC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol
index 46311b750..b6e9af8a8 100644
--- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol
+++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol
@@ -10,4 +10,5 @@ contract C {
     }
 }
 // ----
+// Warning 6328: (157-172): CHC: Assertion violation might happen here.
 // Warning 7812: (157-172): BMC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/operators/mod_signed.sol b/test/libsolidity/smtCheckerTests/operators/mod_signed.sol
index 552e304dd..8588fcf9a 100644
--- a/test/libsolidity/smtCheckerTests/operators/mod_signed.sol
+++ b/test/libsolidity/smtCheckerTests/operators/mod_signed.sol
@@ -10,3 +10,4 @@ contract C {
 	}
 }
 // ----
+// Warning 6328: (163-180): CHC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol b/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol
index 1681c0ca5..4cb63ac44 100644
--- a/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol
+++ b/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol
@@ -12,6 +12,9 @@ contract C {
 	}
 }
 // ----
+// Warning 6328: (221-253): CHC: Assertion violation might happen here.
+// Warning 6328: (257-289): CHC: Assertion violation might happen here.
+// Warning 6328: (293-326): CHC: Assertion violation might happen here.
 // Warning 4661: (221-253): BMC: Assertion violation happens here.
 // Warning 4661: (257-289): BMC: Assertion violation happens here.
 // Warning 4661: (293-326): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/slice_default_start.sol b/test/libsolidity/smtCheckerTests/operators/slice_default_start.sol
index 61aa3ba2a..79de4639c 100644
--- a/test/libsolidity/smtCheckerTests/operators/slice_default_start.sol
+++ b/test/libsolidity/smtCheckerTests/operators/slice_default_start.sol
@@ -9,5 +9,6 @@ contract C {
 	}
 }
 // ----
+// Warning 6328: (157-189): CHC: Assertion violation might happen here.
 // Warning 6328: (193-225): CHC: Assertion violation happens here.
 // Warning 4661: (157-189): BMC: Assertion violation happens here.