pretty-print the term causing smt errors

[lisandrasilva]

Related: https://github.com/runtimeverification/kontrol/issues/21

When the proof crashes due to an SMT error, the term causing it is printed out. However, in most cases, the term is hard to read. It would be helpful to pretty-print the term so users can more easily reason about it and perhaps write lemmas that can simplify it and solve the error.

Example of an SMT error:

ERROR 2024-02-27 09:56:44,308 kevm_pyk.utils - Proof crashed: test%PrimalityCheck.factor(uint256,uint256):0
Smt solver error | code: 5 | data: {'format': 'KORE', 'version': 1, 'term': {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'false'}, 'second': {'tag': 'App', 'name': "Lbl'Unds'andBool'Unds'", 'sorts': [], 'args': [{'tag': 'App', 'name': "LblnotBool'Unds'", 'sorts': [], 'args': [{'tag': 'App', 'name': "Lbl'UndsEqlsEqls'Int'Unds'", 'sorts': [], 'args': [{'tag': 'EVar', 'name': "VarVV0'Unds'x'Unds'114b9705", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}, {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '0'}]}]}, {'tag': 'App', 'name': "Lbl'Unds-LT-'Int'Unds'", 'sorts': [], 'args': [{'tag': 'App', 'name': "Lbl'UndsSlsh'Int'Unds'", 'sorts': [], 'args': [{'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '115792089237316195423570985008687907853269984665640564039457584007913129639935'}, {'tag': 'EVar', 'name': "VarVV0'Unds'x'Unds'114b9705", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}]}, {'tag': 'EVar', 'name': "VarVV1'Unds'y'Unds'114b9705", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}]}]}}, {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-'Int'Unds'", 'sorts': [], 'args': [{'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '1'}, {'tag': 'EVar', 'name': "VarVV0'Unds'x'Unds'114b9705", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}]}}, {'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-'Int'Unds'", 'sorts': [], 'args': [{'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '1'}, {'tag': 'EVar', 'name': "VarVV1'Unds'y'Unds'114b9705", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}]}}]}]}, {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-'Int'Unds'", 'sorts': [], 'args': [{'tag': 'EVar', 'name': "VarCALLER'Unds'ID", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}, {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '1461501637330902918203684832716283019655932542976'}]}}, {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-'Int'Unds'", 'sorts': [], 'args': [{'tag': 'EVar', 'name': "VarID'Unds'CELL", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}, {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '1461501637330902918203684832716283019655932542976'}]}}, {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-'Int'Unds'", 'sorts': [], 'args': [{'tag': 'EVar', 'name': "VarORIGIN'Unds'ID", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}, {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '1461501637330902918203684832716283019655932542976'}]}}, {'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-'Int'Unds'", 'sorts': [], 'args': [{'tag': 'EVar', 'name': "VarTIMESTAMP'Unds'CELL", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}, {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '115792089237316195423570985008687907853269984665640564039457584007913129639936'}]}}]}]}]}]}, {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-'Int'Unds'", 'sorts': [], 'args': [{'tag': 'EVar', 'name': "VarVV0'Unds'x'Unds'114b9705", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}, {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '973013'}]}}, {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-'Int'Unds'", 'sorts': [], 'args': [{'tag': 'EVar', 'name': "VarVV0'Unds'x'Unds'114b9705", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}, {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '115792089237316195423570985008687907853269984665640564039457584007913129639936'}]}}, {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-'Int'Unds'", 'sorts': [], 'args': [{'tag': 'EVar', 'name': "VarVV1'Unds'y'Unds'114b9705", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}, {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '973013'}]}}, {'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-'Int'Unds'", 'sorts': [], 'args': [{'tag': 'EVar', 'name': "VarVV1'Unds'y'Unds'114b9705", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}, {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '115792089237316195423570985008687907853269984665640564039457584007913129639936'}]}}]}]}, {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-Eqls'Int'Unds'", 'sorts': [], 'args': [{'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '0'}, {'tag': 'EVar', 'name': "VarCALLER'Unds'ID", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}]}}, {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-Eqls'Int'Unds'", 'sorts': [], 'args': [{'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '0'}, {'tag': 'EVar', 'name': "VarID'Unds'CELL", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}]}}, {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-Eqls'Int'Unds'", 'sorts': [], 'args': [{'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '0'}, {'tag': 'EVar', 'name': "VarNUMBER'Unds'CELL", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}]}}, {'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-Eqls'Int'Unds'", 'sorts': [], 'args': [{'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '0'}, {'tag': 'EVar', 'name': "VarORIGIN'Unds'ID", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}]}}]}]}, {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-Eqls'Int'Unds'", 'sorts': [], 'args': [{'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '0'}, {'tag': 'EVar', 'name': "VarTIMESTAMP'Unds'CELL", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}]}}, {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-Eqls'Int'Unds'", 'sorts': [], 'args': [{'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '0'}, {'tag': 'EVar', 'name': "VarVV0'Unds'x'Unds'114b9705", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}]}}, {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-Eqls'Int'Unds'", 'sorts': [], 'args': [{'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '0'}, {'tag': 'EVar', 'name': "VarVV1'Unds'y'Unds'114b9705", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}]}}, {'tag': 'And', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'patterns': [{'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'value': 'true'}, 'second': {'tag': 'App', 'name': "Lbl'Unds-LT-Eqls'Int'Unds'", 'sorts': [], 'args': [{'tag': 'EVar', 'name': "VarNUMBER'Unds'CELL", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}, {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '57896044618658097711785492504343953926634992332820282019728792003956564819967'}]}}, {'tag': 'Equals', 'argSort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'sort': {'tag': 'SortApp', 'name': 'SortBool', 'args': []}, 'first': {'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '0'}, 'second': {'tag': 'App', 'name': "Lblchop'LParUndsRParUnds'WORD'Unds'Int'Unds'Int", 'sorts': [], 'args': [{'tag': 'App', 'name': "Lbl'Unds'-Int'Unds'", 'sorts': [], 'args': [{'tag': 'DV', 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}, 'value': '973013'}, {'tag': 'App', 'name': "Lbl'UndsStar'Int'Unds'", 'sorts': [], 'args': [{'tag': 'EVar', 'name': "VarVV0'Unds'x'Unds'114b9705", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}, {'tag': 'EVar', 'name': "VarVV1'Unds'y'Unds'114b9705", 'sort': {'tag': 'SortApp', 'name': 'SortInt', 'args': []}}]}]}]}}]}]}]}]}]}]}]}]}]}}

Steps to reproduce it:

1. checkout the branch lis/smt-error from Kontrol
2. cd src/tests/smt-error
3. run kontrol build
4. run kontrol prove --match-test factor

[palinatolmach]

Related: https://github.com/runtimeverification/kontrol/issues/21

[ehildenb]

• The file kore/rpc.py has SMTSolverError as a return type: https://github.com/runtimeverification/pyk/blob/6fbcf413a8c9058241e8d7aa26dc5a4020c010ff/src/pyk/kore/rpc.py#L424. This error is carrying a Pattern, which is a Kore term.
• Here, when we make an RPC request, we are raise ing a KoreClientError (which can be an SMTSolverError): https://github.com/runtimeverification/pyk/blob/6fbcf413a8c9058241e8d7aa26dc5a4020c010ff/src/pyk/kore/rpc.py#L906.
• Here, in CTermSymbolic (in cterm/symbolic.py) https://github.com/runtimeverification/pyk/blob/6fbcf413a8c9058241e8d7aa26dc5a4020c010ff/src/pyk/cterm/symbolic.py#L68, we have a call to the execute endpoint of the RPC server. But where the call to the RPC server is made, we are not handling any exceptions that the server can throw.

Instead, we can put the call to the RPC server in a try ... except ...: block, so that we can catch the raised error and pretty print the kore term. Something like this:

try:
    response = self._kore_client.execute(...)
except SMTSolverError as err:
    pretty_print(err.pattern)

The file symbolic.py can't do pretty-printing right now, because it doesn't have a pretty printer. Options are:

• Import the PrettyPrinter class from kast.pretty, then do something like:

kast = self.kore_to_kast(err.pattern)
pretty_pattern = PrettyPrinter(self._definition).print(kast)
sys.stderr.write(f'{pretty_pattern}')

• Or propagate the error up:
  • Modify the CTermExecute return type to allow returning also an error result. For example, subclass CTermExecute into CTermExecuteSuccess aond CTermExecuteFailure, and pass the SMTSolverError up in the CTermExecuteFailure.
  • Go to places where cterm_symbolic.execute is used (one example: https://github.com/runtimeverification/pyk/blob/6fbcf413a8c9058241e8d7aa26dc5a4020c010ff/src/pyk/kcfg/explore.py#L161), and modify those locations to handle the failure information.

[ehildenb]

To force the smt solver to timeout, make sure to pass --smt-timeout 10 or something very small.