| Age | Commit message (Collapse) | Author |
|---|
|
Rather than having a global symbol generating function gensym used
throughout the C backend, instead 'generate' them as needed like:
let (gensym, reset_gensym_counter) = symbol_generator "gs"
This just makes things a bit neater and means we can reset the counter
between definitions in jib_compile without worrying about other modules
relying on global uniqueness
|
|
|
|
|
|
|
|
|
|
bitvectors in C
Assumes a Sail C library that has functions with the right types to
support this. Currently lib/int128 supports the -Ofixed_int option,
which was previously -Oint128.
Add a version of Sail C library that can be built with -nostdlib and
-ffreestanding, assuming the above options. Currently just a header
file without any implementation, but with the right types
|
|
|
|
|
|
|
|
|
|
|
|
for 'exception.sail' test that deliberately exits with uncaught exception.
|
|
|
|
|
|
|
|
|
|
|
|
Insert coercions for AV_cval if neccessary
Simplify any n in 2 ^ n, to make sure we can always evaluate 2 ^ n when
n is a constant before passing it to the SMT solver.
|
|
Add a test case for this
|
|
|
|
Clean up ott grammar a bit
|
|
|
|
|
|
|
|
|
|
Allow conversion between int(n) and int in smt_conversion
|
|
|
|
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
|
|
Only change that should be needed for 99.9% of uses is to change
vector('n, 'ord, bit) to bitvector('n, 'ord), and adding
$ifndef FEATURE_BITVECTOR_TYPE
type bitvector('n, dec) = vector('n, dec, bit)
$endif
for to support any Sail before this
Currently I have all C, Typechecking, and SMT tests passing, as well
as the RISC-V spec building OCaml and C completely unmodified.
|
|
|
|
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.
|
|
|
|
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.
|
|
|
|
Jib_compile now has an option that lets it generate real value
literals (VL_real), which we don't want for backends (i.e. C), which
don't support them. Reals are encoded as actual reals in SMT, as there
isn't really any nice way to encode them as bitvectors. Currently we
just have the pure real functions, functions between integers and
reals (i.e. floor, to_real, etc) are not supported for now.
Strings are likewise encoded as SMTLIB strings, for similar reasons.
Jib_smt has ctx.use_real and ctx.use_string which are set when we
generate anything real or string related, so we can keep the logic as
Arrays+Bitvectors for most Sail that doesn't require either.
|
|
|
|
|
|
Only requires a very small change to c_backend.ml. Most of this commit
is duplication of the builtins and runtime in lib/int128. But the
actual differences in those files is also fairly minor could be
handled by some simple ifdefs for the integer builtins.
|
|
|
|
Fixes C backend optimizations that were disabled due to changes in the
IR while working on the SMT generation.
Also add a -Oaarch64_fast option that optimizes any integer within a
struct to be an int64_t, which is safe for the ARM v8.5 spec and
improves performance significantly (reduces Linux boot times by 4-5
minutes). Eventually this should probably be a directive that can be
attached to any arbitrary struct/type.
Fixes the -c_specialize option for ARM v8.5. However this only gives a
very small performance improvment for a very large increase in
compilation time however.
|
