| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
this is implemented in lib/vector_dec.sail as sail function that calls not_vec on sail_zeros.
|
|
|
|
|
|
|
|
|
|
Allow conversion between int(n) and int in smt_conversion
|
|
|
|
|
|
|
|
|
|
Previously we only checked at atom, now use destruct_atom_nexp to pick
up implicit too.
|
|
Also add a $suppress_warnings directive that ensures that no warnings
are generated for a specific file.
|
|
We want to ensure simplication can treat these separately so we
don't accidentally simplify away dependencies between reads and write
addresses.
|
|
|
|
Add path conditions to memory events
Allow simplication of generated SMT based on constructor kinds
|
|
Used to output duplicate type variables in some cases.
|
|
Usually we do this at function applications and casts, but occasionally
a variable is used at a different type.
|
|
are"
This reverts commit 8bed4e4ef414f93e02f28f0e5eb223a855ba3d14.
|
|
|
|
Only checks the leaves that were added in each add_edge/add_edges call.
Slicing bits of the 8.5 model went (for me) from intractable to about
one second.
|
|
The former is useful when a bitvector variable is cast to an equivalent
length, and the latter is easier for Coq's unification to deal with.
|
|
|
|
sane, and an incomplete check on undefined literals.
|
|
|
|
|
|
Expose AST -> Jib compilation function for SMT, and smt_header function
Functorise the optimiser so it can output the SMT definitions to
any data structure
|
|
Generate addresses, kinds, and values separately for read and write
events.
Add an mli interface for jib_smt.ml
|
|
|
|
Allows us to mix generated SMT for two separate threads without name
clashes, however we do want to be able to share datatypes so they are
not prefixed. Currently the pretty-printer adds the prefix but we may
want a smt_def -> smt_def renaming function instead.
|
|
Since we have __deref to desugar *x in this file (as it's the one file
everything includes) we might as well add a __bitfield_deref here too,
for the bitfield setters.
Make sure undefined_nat can be used in C
Both -memo_z3 and -no_memo_z3 were listed as default options, now only
-no_memo_z3 is listed as the default.
|
|
|
|
|
|
Fixes #46
|
|
can now write e.g.
forall (constant 'n : Int) rather than forall ('n: Int)
which requires 'n to be a constant integer value whenever the function
is called. I added this to the 'addrsize variable on memory
reads/writes to absolutely guarantee in the SMT generation that we
don't have to worry about the address being a variable length
bitvector.
|
|
|
|
|
|
|
|
* Includes adding support for bitlist-Lem
* Adds new command-line option -Ofast_undefined
|
|
|
|
|
|
|
|
Generate SMT where the memory reads and writes are totally
unconstrained, allowing additional constraints to be added that
restrict the possible reads and writes based on some memory model.
|
|
|
|
|
|
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.
|
|
Previously path conditionals for a node were defined as the path
conditional of the immediate dominator (+ a guard for explicit guard
nodes after conditional branches), whereas now they are the path
conditional of the immediate dominator plus an expression
encapsulating all the guards between the immediate dominator and the
node. This is needed as the previous method was incorrect for certain
control flow graphs.
This slows down the generated SMT massively, because it causes the
path conditionals to become huge when the immediate dominator is far
away from the node in question. It also changes computing path
conditionals from O(n) to O(n^2) which is not ideal as our inlined
graphs can become massive. Need to figure out a better way to generate
minimal path conditionals between the immediate dominator and the
node.
I upped the timeout for the SMT tests from 20s to 300s each but this
may still cause a failure in Jenkins because that machine is slow.
|
|
|
