Allow witnesses as arguments to bsst-assert

README.md

@@ -117,6 +117,8 @@ position in the script it resides on, while the later is detected afterwards, wh
 
 A data reference can be supplied as argument, like `// bsst-assert(&ref):` or `// bsst-assert-size(&ref):`, and then the target of the assertion will be this data reference instead of the top of the stack. The assertion will be checked at the place where the assetion itself is declared, not at the place where the data reference is declared.
 
+A witness name in the form of `wit<N>` where `<N>` is a number, is also accepted as assertion argument. The witness must be referenced by the script at the time when assertion is checked, otherwise the assertion will be ignored (with a warning)
+
 #### Assertion expression syntax
 
 After `:`, a whitespace-separated list of expressions is expected,

bsst/__init__.py

@@ -5425,19 +5425,36 @@ def apply_bsst_assn(ctx: ExecContext, assn: BsstAssertion | BsstAssumption,
         is_assumption = False
         dref_name = assn.dref_name
 
-    if not top and not dref_name:
-        ctx.add_warning(f"Assertion at line {assn.line_no} ignored "
-                        f"because stack was empty")
-        return
+    def ign_assertion_warning(cause: str) -> None:
+        env.solving_log_ensure_newline()
+        env.solving_log(f'WARNING: ignored assertion @L{assn.line_no}: "{assn.text}" '
+                        f'because {cause}')
+        ctx.add_warning(f"Assertion at line {assn.line_no} ignored because {cause}")
 
-    if dref_name and dref_name not in ctx.data_references:
-        ctx.add_warning(f"Assertion at line {assn.line_no} ignored "
-                        f"because data reference was not found")
+    if not top and not dref_name:
+        ign_assertion_warning('stack was empty')
         return
 
     if dref_name:
-        target = ctx.data_references[dref_name]
-        target_txt = f'{dref_name} = {target}'
+        if dref_name.startswith('&'):
+            if dref_name[1:] not in ctx.data_references:
+                ign_assertion_warning('data reference was not found')
+                return
+
+            target = ctx.data_references[dref_name[1:]]
+            target_txt = f'{dref_name} = {target}'
+        else:
+            m = re.match('wit(\\d+)$', dref_name)
+            assert m, 'only witnesses must be without "&" prefix'
+            wit_no = int(m.group(1))
+            if wit_no >= len(ctx.used_witnesses):
+                ign_assertion_warning(f'witness {dref_name} was not used at this point')
+                return
+
+            target = ctx.used_witnesses[wit_no]
+            assert target.name == dref_name
+            target_txt = target.name
+
     else:
         assert top is not None
         target = top
@@ -5492,7 +5509,7 @@ def symex_op(ctx: ExecContext, op_or_sd: OpCode | ScriptData) -> bool:
     try:
         with CurrentOp(op_or_sd):
             was_executed = _symex_op(ctx, op_or_sd)
-            if was_executed:
+            if was_executed and all(ctx.vfExec):
                 check_bsst_assertions_and_assumptions(ctx)
     except ScriptFailure as sf:
         ctx.register_failure(ctx.pc, str(sf))
@@ -8207,9 +8224,11 @@ def die(msg: str) -> NoReturn:
                             die('unexpected format for bsst-assert')
                         assn_dref_name = assn_arg[1:-1]
                         if not assn_dref_name.startswith('&'):
-                            die('only data references are recognized as arguments to bsst-assert, '
-                                'and data reference name must be prefixed with "&"')
-                        assn_dref_name = assn_dref_name[1:]
+                            if not re.match('wit(\\d+)$', assn_dref_name):
+                                die('only data references and witnesses are recognized '
+                                    'as arguments to bsst-assert, data reference names '
+                                    'must be prefixed with "&", and witness names must have '
+                                    'format "wit<N>" where N is a number')
                     else:
                         assn_dref_name = ''
 
@@ -8287,6 +8306,10 @@ def die(msg: str) -> NoReturn:
             if "'" in data_reference:
                 die("apostrophe <<'>> is not allowed in data reference names")
 
+            if re.match('wit(\\d+)$', data_reference):
+                die('cannot use the name "wit<N>" (where <N> is a number) as '
+                    'data reference, because this name is reserved for witnesses')
+
             seen_data_reference_names[data_reference] = line_no
             data_reference_positions[op_pos] = data_reference
 

release-notes.md

@@ -2,10 +2,12 @@
 
 Version 0.1.2.dev0:
 
-* Add ability to set assertions on stack values and assumptions for data placeholders. Please see newly added "Assertions" and "Assumptions" sections in README. You might also look at `tests/test_assertions_and_assumptions.py` for examples of usage
+* Add ability to set assertions on stack values and witnesses, and assumptions for data placeholders. Please see newly added "Assertions" and "Assumptions" sections in README. You might also look at `tests/test_assertions_and_assumptions.py` for examples of usage
 
 * Fix: scriptnum decoding was not imposing "0 >= x => 255" bound on the byte sequence if its size was 1. This was causing problems with `bsst-assume` tests, but likely that this could have caused problems elsewhere, too
 
+* To avoid confusion, data reference names cannot be "wit<N>" (where <N> is a number), because such names are reserved for witnesses
+
 * Fixes in parser: quotes within quotes were allowed, but should not; angle brackets were sometimes not ignored
 
 * Fix: data placholders with same names should be assumed equal, but were not

tests/test_assertions_and_assumptions.py

@@ -163,23 +163,23 @@ def FreshEnv(*, z3_enabled: bool
     ),
 ]
 
-testcases_assnfail: list[tuple[str, set[int]]] = [
+testcases_assnfail: list[tuple[str, set[int], bool]] = [
     (
         # conflicting assumption constraints
         """
         // bsst-assume($a): 100 1000 43345 -245 -3344 -48394 -4839433545
         // bsst-assume($a): 3
         $a
         """,
-        {2, 3}
+        {2, 3}, False
     ),
     (
         """
         // bsst-assume($a): 100 -4839433545
         $a 0 ADD
         // bsst-assert: 1
         """,
-        {4}
+        {4}, False
     ),
     (
         """
@@ -189,7 +189,7 @@ def FreshEnv(*, z3_enabled: bool
         $a
         // bsst-assert-size: 0
         """,
-        {6}
+        {6}, False
     ),
     (
         """
@@ -199,39 +199,39 @@ def FreshEnv(*, z3_enabled: bool
         $a
         // bsst-assert: !=0
         """,
-        {6}
+        {6}, False
     ),
     (
         """
         // bsst-assume($a): -1..2
         $a
         // bsst-assert: -3..-2
         """,
-        {4}
+        {4}, False
     ),
     (
         """
         // bsst-assume($a): le64(-1)..le64(2)
         $a
         // bsst-assert: le64(-4)..le64(-2)
         """,
-        {4}
+        {4}, False
     ),
     (
         """
         // bsst-assume($a): x('efcdab99')
         $a 0x78563412 CAT
         // bsst-assert: le64(123)
         """,
-        {4}
+        {4}, False
     ),
     (
         """
         // bsst-assume($a): 'abc'
         $a 'def' CAT
         // bsst-assert: 'ABCDEF'
         """,
-        {4}
+        {4}, False
     ),
     (
         """
@@ -242,7 +242,7 @@ def FreshEnv(*, z3_enabled: bool
         // bsst-assert: <22
         // bsst-assert: =19
         """,
-        {7}
+        {7}, False
     ),
     (
         """
@@ -251,7 +251,7 @@ def FreshEnv(*, z3_enabled: bool
         // bsst-assert: le64(10) le64(11) !=le64(12)
         // bsst-assert: =le64(12)
         """,
-        {5}
+        {5}, False
     ),
     (
         """
@@ -266,7 +266,7 @@ def FreshEnv(*, z3_enabled: bool
         // bsst-assert-size: 8
         DROP
         """,
-        {9}
+        {9}, False
     ),
     (
         """
@@ -275,7 +275,7 @@ def FreshEnv(*, z3_enabled: bool
         1 ADD
         // bsst-assert: 1
         """,
-        {3}
+        {3}, False
     ),
     (
         """
@@ -286,21 +286,37 @@ def FreshEnv(*, z3_enabled: bool
         1 ADD 258 NUMEQUALVERIFY
         // bsst-assert(&a): 0x00
         """,
-        {7}
+        {7}, False
     ),
     (
         """
-        DUP // =>a
+        DUP
         IF
-        10 GREATERTHAN
+        // bsst-assert-size: >0
+        DUP 1 GREATERTHANOREQUAL VERIFY
         ELSE
-        // bsst-assert-size: 10
+        // bsst-assert-size: 1
         SIZE 10 NUMEQUALVERIFY
         ENDIF
+        // bsst-assert(wit0): 1
         // bsst-assert: >10
-        // bsst-assert(&a): 0
         """,
-        {6, 10}
+        {7, 11}, True
+    ),
+    (
+        """
+        DUP
+        IF
+        // bsst-assert-size: >0
+        DUP 1 GREATERTHANOREQUAL VERIFY
+        ELSE
+        // bsst-assert-size: 1
+        SIZE 10 NUMEQUALVERIFY
+        ENDIF
+        // bsst-assert: >0
+        // bsst-assert(wit0): 0
+        """,
+        {7, 11}, True
     ),
 ]
 
@@ -338,6 +354,11 @@ def FreshEnv(*, z3_enabled: bool
     """
     1
     // bsst-assert: 2..1
+    """,
+    # non-witness name for bsst-assert name without &
+    """
+    1 // =>wit
+    // bsst-assert(wit): 1
     """
 ]
 
@@ -401,7 +422,7 @@ def post_finalize_hook(ctx: bsst.ExecContext,
 
 
 def test_assn_failing(
-    tc_no: int, tc_text: str, failure_lines: set[int]
+    tc_no: int, tc_text: str, failure_lines: set[int], is_exact_match: bool
 ) -> None:
 
     with FreshEnv(z3_enabled=True) as env:
@@ -438,14 +459,17 @@ def search_failures(ctx: bsst.ExecContext) -> None:
                 fl = int(m.group(1))
                 flines.add(fl)
 
-            assert flines.issubset(failure_lines)
+            assert flines.issubset(failure_lines), (flines, failure_lines)
             seen_failure_lines.update(flines)
 
         env.get_root_branch().walk_contexts(search_failures,
                                             include_failed=True)
 
         assert seen_failure_lines, "at least one failure must be detected"
         assert seen_failure_lines.issubset(failure_lines)
+        if is_exact_match:
+            assert seen_failure_lines == failure_lines, \
+                ("exact match expected", seen_failure_lines, failure_lines)
 
         print("OK")
 
@@ -473,9 +497,10 @@ def test_other_failing(tc_no: int, tc_text: str) -> None:
         print("TESTCASE ASSN NORMAL", tc_no+1, end=' ')
         test_assn_normal(tc_no, tc_text, tc_expected_values)
 
-    for tc_no, (tc_text, failure_lines) in enumerate(testcases_assnfail):
+    for tc_no, (tc_text, failure_lines, is_exact_match) in \
+            enumerate(testcases_assnfail):
         print("TESTCASE ASSN FAILING", tc_no+1, end=' ')
-        test_assn_failing(tc_no, tc_text, failure_lines)
+        test_assn_failing(tc_no, tc_text, failure_lines, is_exact_match)
 
     for tc_no, tc_text in enumerate(testcases_otherfail):
         print("TESTCASE OTHER FAILING", tc_no+1, end=' ')