Module isla_axiomatic::footprint_analysis

This module implements footprint analysis for the concurrency tool

The axiomatic memory model requires deriving (syntactic) address, data, and control dependencies. As such, we need to know what registers could be touched by each instruction based purely on its concrete opcode. For this we analyse all the traces from a litmus test run, and use symbolic execution on each opcode again.

Structs

Footprint
Footprintkey

Enums

FootprintError

Functions

addr_dep	Returns true if there exists an RR or RW address dependency from instrs[from] to instrs[to].
ctrl_dep	Returns true if there exists an RW or RR control dependency from instrs[from] to instrs[to].
data_dep	Returns true if there exists an RW data dependency from instrs[from] to instrs[to].
footprint_analysis	Arguments
rmw_dep