simplification_check Namespace Reference

Debug-mode guard on the expression simplifier (esbmc/esbmc#4625). More...

Namespaces
namespace	detail

Typedefs
using	checkert
	Called for every rewrite the simplifier performs.

Functions
void	install (checkert checker)
void	clear ()
	Uninstall, restoring the inert default.
void	verify_rewrite (const expr2tc &before, const expr2tc &after)
	Consult the installed checker.
void	verify_node_rewrite (const expr2t &before, const expr2tc &after)
	As above, where the rewritten node exists only as this.
void	verify_rewrite_or_node (const expr2tc &before, const expr2t &node, const expr2tc &after)
	As above, for a caller that holds the rewritten node in a container only sometimes – a nil before means clone node instead.

Detailed Description

Debug-mode guard on the expression simplifier (esbmc/esbmc#4625).

simplify() lives in irep2, which links only fmt/bigint/immer – not the solvers, and not util. The SMT query therefore cannot be issued from here. Instead the driver installs a checker once it holds a namespace and options, and simplify() consults whatever is installed. Nothing is installed by default, so the hook is inert in a normal run even when the build enabled it.

The hook is consulted per node, at the point each rewrite is made, rather than once per outermost call (esbmc/esbmc#7260): a peephole is what changes meaning, and checking whole expressions saw neither the peepholes nor the direct expr2t::simplify() callers that never reach the free simplify() below. Coverage is still not total, and three gaps are structural: simplify() returns nil for address_of before any rewrite site (overflow now reaches one narrow rewrite – the widened-operand-multiply overflow shortcut in overflow2t::do_simplify() (#7840) – but is_unstatable_shape() declines it explicitly: stating it as an equality would hand the checker's solver back the exact double-width multiply the shortcut exists to keep away from the solver); the driver cannot install a checker until it holds a namespace, so frontend parsing runs unchecked; and the rewrites the checker's own solver performs are skipped by the reentrancy guard below, counted in neither total. A fourth gap, check() declining a shape it cannot state as an equality, is the one the declined counter makes visible.

Typedef Documentation

checkert

using simplification_check::checkert

Initial value:

 
  std::function<void(const expr2tc &before, const expr2tc &after)>

Called for every rewrite the simplifier performs.

Reporting a mismatch – logging, aborting – is the checker's business, not the hook's.

Function Documentation

clear()

void simplification_check::clear

(

)

Uninstall, restoring the inert default.

install()

void simplification_check::install

(

checkert

checker

)

verify_node_rewrite()

void simplification_check::verify_node_rewrite ( const expr2t & before, const expr2tc & after )

inline

As above, where the rewritten node exists only as this.

The clone is inside the guard: it is the whole cost of the call, and a normal build must not pay it.

verify_rewrite()

void simplification_check::verify_rewrite ( const expr2tc & before, const expr2tc & after )

inline

Consult the installed checker.

Compiled out entirely unless the build was configured with -DENABLE_SIMPLIFIER_EQUIVALENCE_CHECK=ON: the simplifier runs on every expression ESBMC builds, so an unconditional indirect call would be a permanent tax on a debug aid.

verify_rewrite_or_node()

void simplification_check::verify_rewrite_or_node ( const expr2tc & before, const expr2t & node, const expr2tc & after )

inline

As above, for a caller that holds the rewritten node in a container only sometimes – a nil before means clone node instead.

Choosing between them here rather than at the call site keeps the branch out of simplify(), which the complexity gate gives no room to grow.