Module simplify

Expand description

This module implements various routines for simplifying event traces, as well as printing the generated traces.

Structs§

EventReferences: The EventReferences struct contains for every variable v in a trace, the set of all it’s immediate dependencies, i.e. all the symbols used to directly define v, as computed by uses_in_exp.
WriteOpts: Options for writing event traces

commute_extract: This rewrite pushes extract expressions inwards where possible, so
eval: Evaluate SMT subexpressions if all their arguments are constant
hide_initialization: Removes register effects from before the first (cycle) event. When combined with remove_unused this will reduce the amount of initialization that appears in the trace.
propagate_forwards_used_once: This rewrite looks for events of the form (define-const v (expression)), and if v is only used exactly once in subsequent events it will replace that use of v by the expression.
remove_unused: Removes SMT events that are not used by any observable event (such as a memory read or write).
renumber_event: renumber_event Renumbers all the symbolic variables in an event such that multiple event sequences can have disjoint variable identifiers. It takes two u32 arguments i and total, such that i is the index of our event sequence in the range 0..(total - 1) inclusive where total is the number of event sequences we want to make disjoint.
write_events
write_events_with_opts