LARA

Interpreting Control-Flow Graphs

Standard Execution

Running

i = 0;
while (i < 5) {
  i = i + 1;
}

Running Collatz example

A path through graph

A trace for a given path: add states of variables

An execution trace through control-flow graph

Computing Reachable States by Execution

One way: by deterministic execution, store the states

Example

Collecting Reachable States

Another way: updating set of reachable states until they stabilize

This is useful if we have non-determinism

  • unknown inputs
  • like NDFA

Analysis is similar to execution

  • when analyzing, we will not know exact values of variables
  • we wish to check for all possible initial state of e.g. procedure

This is called “collecting semantics”

Equations for collecting semantics

  • recall one step operational semantics
  • here we have semantics for basic commands
  • they are then propagated through the graph