| Age | Commit message (Collapse) | Author |
|---|
|
Add path conditions to memory events
Allow simplication of generated SMT based on constructor kinds
|
|
Effectively reverts 7280e7b with a different method that isn't slow,
although it's not totally clear that this is correct - it could just
be more subtly wrong than before commit 7280e7b.
Following is mostly so I can remember what I did to document & write
up properly at some point:
What we do is compute 'pi' conditions as before by traversing the
dominator tree, we each node having a pi condition defined as the
conjunction of all guards between it and the start node in the
dominator tree. This is imprecise because we have situations like
1
/ \
2 3
| |
| 4
| |\
5 6 9
\ / |
7 10
|
8
where 8 = match_failure, 1 = start and 10 = return.
2, 3, 6 and 9 are guards as they come directly after a control flow
split, which always follows a conditional jump.
Here the path through the dominator tree for the match_failure is
1->7->8 which contains no guards so the pi condition would be empty.
What we do now is walk backwards (CFG must be acyclic at this point)
until we hit the join point prior to where we require a path
condition. We then take the disjunction of the pi conditions for the
join point's predecessors, so 5 and 6 in this case. Which gives us a
path condition of 2 | (3 & 6) as the dominator chains are 1->2->5 and
1->3->4->6.
I think this works as any split in the control flow must have been
caused by a conditional jump followed by distinct guards, so each of
the nodes immediately prior to a join point must be dominated by at
least one unique guard. It also explains why the pi conditions seem
sufficient to choose outcomes of phi functions.
If we hit a guard before a join (such as 9 for return's path
conditional) we just return the pi condition for that guard, i.e.
(3 & 9) for 10. If we reach start then the path condition is simply
true.
|
|
Makes the graph slightly cleaner, and means we can represent
conditionals in a way that shoud allow computing path conditions much
easier.
Essentially rather than a basic block being a list of instructions
where the last instruction is a jump (or other terminator) it is now a
list of instructions combined with an explict terminator, i.e.
CF_block (instrs @ I_jump (cval, label) ==> CF_block (instrs, T_jump (n, label))
Rather than storing the cval in the T_jump it just has a number that
links to a mapping from numbers to cvals, and we represent the
negation of any cval in that table by negating its number. Therefore
at any join point in the CFG, we can efficiently check when the
joining path conditionals contain both n and minus n and remove both.
|
|
|
|
Currently only works with CVC4, test cases are in test/smt. Can prove
that RISC-V add instruction actually adds values in registers and
that's about it for now.
|
|
Allows us to track the last version of the return variable when the AST
in in SSA form.
|
|
Add a test case to ensure variable types in l-expressions remain the
same with flow-sensitive constraints.
|
|
Avoids duplication between l-expressions and expressions. Also means that
special variables like current_exception and have_exception are treated
normally by functions such as instr_reads and instr_writes etc. Furthermore
we can now easily annotate Jib identifiers in ways that were not previously
possible with plain sail ids.
|
|
:def <definition> evaluates a top-level definition
:(b)ind <id> : <type> creates an identifier within the interactive type-checking environment
:let <id> = <expression> defines an identifier
Using :def the following now works and brings the correct vector
operations into scope.
:def default Order dec
:load lib/prelude.sail
Also fix a type-variable shadowing bug
|
|
|
|
Add a CL_void l-expression so we don't have redundant unit-typed
variables everywhere, and add an optimization in Jib_optimize called
optimize_unit which introduces these.
Remove the basic control-flow graph in Jib_util and add a new mutable
control-flow graph type in Jib_ssa which allows the IR to be converted
into SSA form. The mutable graph allows for more efficient updates,
and includes both back and forwards references making it much more
convenient to traverse.
Having an SSA representation should make some optimizations much
simpler, and is also probably more natural for SMT generation where
variables have to be defined once using declare-const anyway.
Debug option -ddump_flow_graphs now outputs SSA'd graphs of the
functions in a specification.
|
