Add `--print-smt` flag to output the SMTChecker SMTLIB code

Abstract

Symbolic execution and formal verification are becoming hotter topics in the web3 & security space. As a community, we are becoming more mature and realizing the current testing status quo isn't enough.

Symbolic execution and formal verification are ways we can combat many issues. Still, it's challenging for people to understand how they work at the moment, and learn how to implement them effectively. Learning language models like ChatGPT have made this barrier easier, but a simple tweak of solidity such as outputting the SMTLIB code it uses for formal verification would make it much easier to teach the concept, and can be helpful for users trying to understand why the SMTChecker is giving the output it is.

Motivation

See above.

It seems like this would be relatively doable, as a simple print statement can achieve the desired result. https://gist.github.com/hrkrshnn/306ebb5fc4687062a6fd865451348137

(Thanks Hari!)

Specification

./solc example.sol --model-checker-engine bmc --print-smt

This would then print the smt code.

(declare-datatypes ((bytes_tuple 0)) (((bytes_tuple (bytes_tuple_accessor_array (Array Int Int)) (bytes_tuple_accessor_length Int)))))
(declare-datatypes ((tx_type 0)) (((tx_type (block.basefee Int) (block.chainid Int) (block.coinbase Int) (block.difficulty Int) (block.gaslimit Int) (block.number Int) (block.timestamp Int) (blockhash (Array Int Int)) (msg.data bytes_tuple) (msg.sender Int) (msg.sig Int) (msg.value Int) (tx.gasprice Int) (tx.origin Int)))))
(declare-fun expr_8_1 () Bool)
(declare-fun tx_0 () tx_type)
(declare-fun x_2_0 () Int)
(declare-fun expr_6_0 () Int)
.
.
.

Backwards Compatibility

Should be backwards compatible.

ethereum / solidity