| Commit message (Collapse) | Author | Age | Files | Lines |
|\
| |
| |
| |
| |
| | |
Conflicts:
Makefile
configure
|
| | |
|
| | |
|
| |\ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Previously, the elimination of useless conditions done in the 2nd pass of the tunneling
introduced some new "nop" instructions that were not eliminated.
This commit solves this issue by anticipating the elimination of conditions in the 1st pass
of the tunneling, the 2nd pass being unchanged.
In case of cycles in the CFG, the full elimination of useless conditions may require several
iterations in the 1st pass. Moreover, in the simulation proof, the measure counting the number of
eliminated steps from each node, needs to be adapted according to the modifications on the 1st pass.
Hence, this measure results from a quite complex fixpoint computation: proving its properties
would be very difficult.
This leads us to introduce an oracle, implementing the first pass and producing the expected
measure. A certified verifier directly checks that the measure provided by the oracle
satisfies the properties expected by the simulation proof.
Introducing this oracle/verifier pair has here the following advantage:
- the proof is simpler than the original one (e.g. having a certified union-find structure
is no more necessary for this pass).
- the oracle is very efficient, by using imperative data-structure to compute memoized
fixpoints.
At runtime, the overhead induced by the verifier computations (and the actual computation of
the measure) seems largely compensated by the gains obtained through the imperative oracle.
|
| |\| |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| |\ \ \ \ \
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Adapting the new mppa-RTLpathSE passes into the new Compiler.vexpand
framework
|
|\ \ \ \ \ \ \
| |_|_|_|_|_|/
|/| | | | | | |
|
| |/ / / / /
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None`
by a call to the function Hashtbl.find_opt.
|
| |_|_|_|/
|/| | | | |
|
| |_|_|/
|/| | | |
|
| |_|/
|/| | |
|
| | | |
|
| |/
|/| |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
|/ |
|
|
|
|
|
|
|
|
| |
Initially, the "bench" entries of the test suite used a "xtime" utility
developed in-house and not publically available.
This commit adds a version of "xtime" written in OCaml (tools/xtime.ml)
and updates the "bench" entries of the test/*/Makefile to use it.
|
|
|
|
|
|
| |
Syntax is "pat ?? bexpr => action".
The whole case is selected only when "pat" matches and then "bexpr"
evaluates to "true".
|
|
|
|
|
|
| |
This is useful to e.g. identify the .vo files from CompCert that a clightgen-generated .v file needs.
Also: the "result" field of the record type is now initialized with the LHS of the dependency, not the RHS. It doesn't matter because the result field is unused, but it makes more sense now.
|
| |
|
| |
|
|
|
|
| |
printing duplicated -I flags.
|
| |
|
|
|
|
| |
Avoids warnings with 4.02.
|
|
|
|
|
|
| |
produce the executables.
configure: add check for GNU make.
|
|
- Most RTL operators now evaluate to Some Vundef instead of None
when undefined behavior occurs.
- More aggressive instruction selection.
- "Bertotization" of pattern-matchings now implemented by a proper preprocessor.
- Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|