|
|
|
@2706
|
8 years |
mckinna |
repaired contentious broken automation
at end of subgoal 9 of case (* …
|
|
|
|
@2705
|
8 years |
sacerdot |
More progress in ASM towards implementing the new pseudoinstructions.
|
|
|
|
@2704
|
8 years |
tranquil |
moved JMP from instructions to preinstructions, and added MovSuccessor? …
|
|
|
|
@2703
|
8 years |
mckinna |
now includes defn of costlabel_map
|
|
|
|
@2702
|
8 years |
sacerdot |
1. proof closed in ASM/UtilBranch
2. more passes integrated in the …
|
|
|
|
@2701
|
8 years |
sacerdot |
Automation failure fixed by replacing with hand made proof.
|
|
|
|
@2700
|
8 years |
sacerdot |
1. exponential function dropped in favour of standard library
2. …
|
|
|
|
@2699
|
8 years |
mckinna |
simplified dependencies somewhat
|
|
|
|
@2698
|
8 years |
mckinna |
simplified dependencies
|
|
|
|
@2697
|
8 years |
sacerdot |
Compiler fixed to include the ERTLptrToLTL pass.
|
|
|
|
@2696
|
8 years |
sacerdot |
I can't get this right... :-(
|
|
|
|
@2695
|
8 years |
sacerdot |
Renamed again.
|
|
|
|
@2694
|
8 years |
tranquil |
completed ERTLptrToLTL
|
|
|
|
@2693
|
8 years |
sacerdot |
1. Stuff moved to correct places.
2. ERTLptr pass added
|
|
|
|
@2692
|
8 years |
garnier |
Add some more constraints in clight_cminor_data.
|
|
|
|
@2691
|
8 years |
sacerdot |
ERTLtoERTLptr* moved to the proper place
|
|
|
|
@2690
|
8 years |
campbell |
Most of the measurable subtrace preservation proof done.
|
|
|
|
@2689
|
8 years |
tranquil |
* fixed passes up to linearisation
|
|
|
|
@2688
|
8 years |
tranquil |
* in Arithmeticcs.ma: commented include that breaks script in latest …
|
|
|
|
@2687
|
8 years |
tranquil |
* polished some interfaces
|
|
|
|
@2686
|
8 years |
mckinna |
two minor modifications to assist disambiguation of "lookup"
file …
|
|
|
|
@2685
|
8 years |
campbell |
Progress on measurable trace preservation: prefix preserves observable …
|
|
|
|
@2684
|
8 years |
sacerdot |
…
|
|
|
|
@2683
|
8 years |
tranquil |
proof of properties of b_graph_program_transform (with an open axiom)
|
|
|
|
@2682
|
8 years |
campbell |
Don't apply inv in after_n_steps to last state.
|
|
|
|
@2681
|
8 years |
tranquil |
* improvements to the graph translation function
* fixed passes up to LTL
|
|
|
|
@2680
|
8 years |
mckinna |
proofs which previously succeeded fail, thanks to fold on positive_map …
|
|
|
|
@2679
|
8 years |
mckinna |
Further tweak to Brian's changes: no normalization reqd at all!
|
|
|
|
@2678
|
8 years |
campbell |
Switch to single source step simulations for front-end measurable …
|
|
|
|
@2677
|
8 years |
campbell |
Retain the pointer for the function called in front-end call states
so …
|
|
|
|
@2676
|
8 years |
campbell |
Less aggressive normalisation in ASMCosts to prevent memory blowup.
|
|
|
|
@2675
|
8 years |
tranquil |
* a generic graph program transformation
|
|
|
|
@2674
|
8 years |
tranquil |
* another change in block definition
* RTLabs -> RTL and ERTL -> …
|
|
|
|
@2673
|
8 years |
tranquil |
corrected some compilation errors (that might depend on some matita update)
|
|
|
|
@2672
|
8 years |
sacerdot |
One less axiom on bitvectors.
|
|
|
|
@2671
|
8 years |
sacerdot |
simplification
|
|
|
|
@2670
|
8 years |
campbell |
Clean up from recent commits.
|
|
|
|
@2669
|
8 years |
campbell |
Tweak exec_steps output; show that simulations extend to measurable …
|
|
|
|
@2668
|
8 years |
campbell |
Intermediate measurable proof check-in before I change its traces again.
|
|
|
|
@2667
|
8 years |
garnier |
Clight to Cminor, statements: some cases down. Subset of the …
|
|
|
|
@2666
|
8 years |
piccolo |
bug fixed in blocks.ma
|
|
|
|
@2665
|
8 years |
sacerdot |
…
|
|
|
|
@2664
|
8 years |
sacerdot |
Tailcall case implemented (it does not happen ATM).
|
|
|
|
@2663
|
8 years |
piccolo |
some minor modifications to ERTLtoERTLptr
|
|
|
|
@2662
|
8 years |
piccolo |
Towards a very generalized lemma that summarizes all of Paolo's results.
|
|
|
|
@2661
|
8 years |
sacerdot |
stacksize "repaired" by "considering" tailcalls
Some daemons added …
|
|
|
|
@2660
|
8 years |
sacerdot |
…
|
|
|
|
@2659
|
8 years |
sacerdot |
Tailcall elimination no longer necessary:
1. the back-end is almost …
|
|
|
|
@2658
|
8 years |
sacerdot |
…
|
|
|
|
@2657
|
8 years |
sacerdot |
Cost proof fully repaired. It was broken by the definitions used in …
|
|
|
|
@2656
|
8 years |
sacerdot |
Ported to tailcalls (currently nothing is classified as a tailcall).
|
|
|
|
@2655
|
8 years |
tranquil |
new step in code semantic lemma
|
|
|
|
@2654
|
8 years |
garnier |
Memory injections in a coherent state.
|
|
|
|
@2653
|
8 years |
sacerdot |
…
|
|
|
|
@2652
|
8 years |
sacerdot |
String type changed definition.
|
|
|
|
@2651
|
8 years |
sacerdot |
Type String changed.
|
|
|
|
@2647
|
8 years |
sacerdot |
Stupid typo fixed.
|
|
|
|
@2646
|
8 years |
sacerdot |
A tag was classified as an error message. Fixed.
|
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
|
@2644
|
8 years |
campbell |
Commit some work on FEMeasurable before trying to do something nicer …
|
|
|
|
@2643
|
8 years |
sacerdot |
We are not proving erasure, so this is dead code.
|
|
|
|
@2642
|
8 years |
piccolo |
fixed joint/Traces after having posed block 0 to be Code
|
|
|
|
@2641
|
8 years |
piccolo |
defined dummy block code equals to 0
|
|
|
|
@2640
|
8 years |
tranquil |
updated RTL and RTLabs to RTL translation
|
|
|
|
@2639
|
8 years |
sacerdot |
We are not going to prove erasure. Thus this becomes dead code.
|
|
|
|
@2638
|
8 years |
piccolo |
Back-end fixes for last Garnier's commit that removes the regions from …
|
|
|
|
@2624
|
8 years |
campbell |
Properly evict unused and axiomatised Floats.
|
|
|
|
@2623
|
8 years |
campbell |
Name change update.
|
|
|
|
@2619
|
8 years |
campbell |
Update some test cases.
|
|
|
|
@2618
|
8 years |
campbell |
Tidy up measurable a little.
|
|
|
|
@2617
|
8 years |
campbell |
Trivial simplification on split_trace.
|
|
|
|
@2608
|
8 years |
garnier |
Regions are no more stored in blocks. block_region now tests the id, …
|
|
|
|
@2604
|
8 years |
piccolo |
ERTLtoERTLptr in place.
|
|
|
|
@2603
|
8 years |
piccolo |
Dead code commented out.
|
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
|
@2600
|
8 years |
garnier |
Memory injections are now only defined relatively to block ids, not …
|
|
|
|
@2599
|
8 years |
tranquil |
* map_opt and map on positive maps are now clean (erase empty …
|
|
|
|
@2598
|
8 years |
garnier |
Tentative, partial draft for the definition of Clight-Cminor …
|
|
|
|
@2597
|
8 years |
campbell |
Some work in progress on measurable subtrace preservation.
|
|
|
|
@2596
|
8 years |
campbell |
Use a simpler stack cost map, and then specialise to each semantics.
|
|
|
|
@2595
|
8 years |
tranquil |
* dropped locals and exit from definition of joint_if_function
* new …
|
|
|
|
@2594
|
8 years |
garnier |
Some fixes in memory injections, and some holes filled.
|
|
|
|
@2593
|
8 years |
mckinna |
Finally chased down wicked failure to close case 1.1: of …
|
|
|
|
@2592
|
8 years |
piccolo |
main lemma of ERTLptr in place
|
|
|
|
@2591
|
8 years |
garnier |
Moved simulation proof for expressions in toCminorCorrectnessExpr.ma, …
|
|
|
|
@2590
|
8 years |
piccolo |
added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc …
|
|
|
|
@2588
|
8 years |
garnier |
modified Cexec/Csem? semantics:
. force andbool and orbool types to be …
|
|
|
|
@2582
|
8 years |
garnier |
Some progress on CL to CM.
|
|
|
|
@2581
|
8 years |
mckinna |
commented out back end entirely until knock-on effects of changes to …
|
|
|
|
@2578
|
8 years |
garnier |
Progress on CL to CM, fixed some stuff in memory injections.
|
|
|
|
@2576
|
8 years |
campbell |
Add conditional test case that also uses switch removal.
|
|
|
|
@2575
|
8 years |
mckinna |
temporary commit
localised the source of trouble in the proof of
…
|
|
|
|
@2574
|
8 years |
campbell |
Update labelling simulation proofs due to some changes elsewhere.
|
|
|
|
@2573
|
8 years |
mckinna |
temporary fixes to ensure {compiler,correctness}.ma recompile
after …
|
|
|
|
@2572
|
8 years |
garnier |
Progress on toCminorCorrectness.
|
|
|
|
@2571
|
8 years |
campbell |
Lots of little changes for cl_tailcall and classifier change.
|
|
|
|
@2570
|
8 years |
piccolo |
ERTLtoERTLptr in place
|
|
|
|
@2569
|
8 years |
campbell |
Fix Clight semantics for ptr + char. (Compiler works anyway.)
|
|
|
|
@2568
|
8 years |
campbell |
Relax some Clight type checks to Cminor type checks to avoid …
|
|
|
|
@2566
|
8 years |
piccolo |
ERTL to ERTLptr pass implemented up to a few things to be
left to the …
|
|
|
|
