fingerprint.h File Reference

#include <cstdint>
#include <string>
#include <goto-symex/equation/symex_target_equation.h>

Include dependency graph for fingerprint.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	ssa_cone_keyt
	A cone's 128-bit key. More...

Enumerations
enum class	fingerprint_modet { raw , srcloc , full }
	Normalisation applied to SSA symbols before a claim's cone is digested. More...

Functions
uint64_t	ssa_cone_digest (const symex_target_equationt::SSA_stepst &steps, fingerprint_modet mode)
	Digest the surviving steps of a per-claim sliced equation.
ssa_cone_keyt	ssa_cone_key (const symex_target_equationt::SSA_stepst &steps, fingerprint_modet mode)
std::string	ssa_cone_key_string (const symex_target_equationt::SSA_stepst &steps, fingerprint_modet mode)
	ssa_cone_key rendered as 32 hex digits.
uint64_t	fingerprint_hash (const std::string &s)
	FNV-1a over s. Stable across processes, unlike irep2's crc().
size_t	ssa_cone_size (const symex_target_equationt::SSA_stepst &steps)
	Number of steps the digest covered.

Enumeration Type Documentation

fingerprint_modet

enum class fingerprint_modet

strong

Normalisation applied to SSA symbols before a claim's cone is digested.

ESBMC bakes a source character offset into every local's name, so a literal digest only ever matches a byte-identical re-run. The normalising modes quantify how much of that instability is recoverable.

Enumerator
raw	No normalisation. Baseline for the measurement.
srcloc	Strip the <file>@<character-offset>@ segment ESBMC bakes into every local's name, re-disambiguating names that collide once it is gone.
full	Alpha-rename every symbol: the digest sees structure and types only.

Function Documentation

fingerprint_hash()

uint64_t fingerprint_hash

(

const std::string &

s

)

FNV-1a over s. Stable across processes, unlike irep2's crc().

ssa_cone_digest()

uint64_t ssa_cone_digest	(	const symex_target_equationt::SSA_stepst &	steps,
		fingerprint_modet	mode )

Digest the surviving steps of a per-claim sliced equation.

Each non-ignored step contributes its type and every expression convert_internal_step hands the solver for it: guard and cond for an assume, assert, branching or assignment, plus lhs/rhs for a renumber and the arguments for an output, neither of which is reachable through cond.

Symbols reachable only through a type (a symbolic array size) are not normalised, which can only cost hits, never manufacture them.

ssa_cone_key()

ssa_cone_keyt ssa_cone_key	(	const symex_target_equationt::SSA_stepst &	steps,
		fingerprint_modet	mode )

ssa_cone_key_string()

std::string ssa_cone_key_string	(	const symex_target_equationt::SSA_stepst &	steps,
		fingerprint_modet	mode )

ssa_cone_key rendered as 32 hex digits.

ssa_cone_size()

size_t ssa_cone_size

(

const symex_target_equationt::SSA_stepst &

steps

)

Number of steps the digest covered.