| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
Outside of -interp mode, -main has no (known) effect but could be
confused for a linker option that sets the program's entrypoint, say.
It's safer to reject the option.
|
| | |
| |
| |
| | |
Inlined built-in functions destroy GPR0
|
| | |
| |
| |
| |
| | |
Pflid destroys IR14
Inlined built-in functions destroy IR14
|
| | |
| |
| |
| |
| |
| | |
Pfmovimms, Pfmovimmd destroy X16
Pbtbl preserves X17
Inlined built-in functions destroy X16 and X30
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Also remove the Ofloatofint, Ofloatofintu, and Ointuoffloat
PowerPC operations.
The pseudoinstructions were used to implement these operations,
as follows:
Pfcfi : Ofloatofint i.e. the conversion signed int32 -> float64
Pfcfiu : Ofloatofintu i.e. the conversion unsigned int32 -> float64
Pfctiu : Ointuoffloat i.e. the conversion float64 -> unsigned int32
These pseudoinstructions were expanded (in Asmexpand.ml) in terms of
Pfcfid : signed int64 -> float64
Pfctidz : float64 -> signed int64
and int32/int64 conversions.
This commit performs this expansion during instruction selection
(SelectOp.vp):
floatofint(n) becomes floatoflong(longofint(n))
floatofintu(n) becomes floatoflong(longuofint(n))
intuoffloat(n) becomes cast32unsigned(longoffloat(n))
Then there is no need for the 3 removed operations and the 3 removed
pseudoinstructions.
More importantly, the correctness of these expansions is now proved as
part of instruction selection, using the corresponding results from
Floats.v.
|
| | | |
|
| |\ \
| | |
| | |
| | |
| | |
| | | |
Conflicts:
Makefile
configure
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
In some cases of two imbricated loops, we would tail-duplicate too much,
because of the input trace traversing both loop headers.
|
| | | | |
|
| | | |
| | |
| | |
| | | |
Happened when a loop was predicted not to be taken
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
Right now though the compilation time is too high for glpk, I need to
figure out why
|
| | | | |
|
| | |\ \
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Conflicts:
arm/Op.v
common/Values.v
kvx/Op.v
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | |\| | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | |\ \
| | | | |
| | | | |
| | | | | |
gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
|
| | | | | | |
|
| | | |/ / |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
proof of the two remaining lemmas
|
| | | | | |
|
| | |\| | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | | |
| | | |
| | | |
| | | | |
helps to understand the difference between union and merge in the interface
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | |\| | |
|
| | |\ \ \ |
|
| | | | | | |
|
| | |\ \ \ \ |
|
| | |\ \ \ \ \ |
|
| | |\ \ \ \ \ \ |
|
