Add some experimental support for non-lexical flow-typing rules

Add a file nl_flow.ml which can analyse a block of Sail expressions
and insert constraints for flow-typing rules which do not follow the
lexical structure of the code (and therefore the syntax-directed
typing rules can't do any flow-typing for). A common case found in ASL
translated Sail would be something like

function decode(Rt: bits(4)) = {
  if Rt == 0xF then {
    throw(Error_see("instruction"));
  };
  let t = unsigned(Rt);
  execute(t)
}

which would currently fail is execute has a 0 <= t <= 14 constraint
for a register it writes to. However if we spot this pattern and add
an assertion automatically:

  let t = unsigned(Rt);
  assert(t != 15);
  execute(t)

Then everything works, because the assertion is in the correct place
for regular flow typing. Currently it only works for this specific
use-case, and is turned on using the -non_lexical_flow flag

0 files changed, 0 insertions, 0 deletions