

@3371

7 years 
piccolo 
Modified RTLsemantics and ERTLsemantics. Now the pop frame will set …



@3265

7 years 
tranquil 
added validate_pointer filter
in Interference added that intereference …



@3263

7 years 
tranquil 
moved callee saved saving and restoring to ERTL > LTL pass (untrusted …



@3262

7 years 
piccolo 
reverted status_simulation_utils



@3261

7 years 
piccolo 
reverted joint_semantics rtl_semantics and ltl_semantics



@3259

7 years 
piccolo 
changed ERTL semantics:
1) added manipulation of stack pointer …



@3257

7 years 
tranquil 
fixed uses in ERTL



@3255

7 years 
tranquil 
* dropped newframe and delframe (to be integrated in calls and returns …



@3253

7 years 
piccolo 
some proof obbligation closed of ERTL to LTL proof



@3252

7 years 
piccolo 
proof obbligation added on ERTL to LTL proof



@3217

7 years 
piccolo 
Correctness of ERTL to LTL in place



@3145

7 years 
tranquil 
* removed sigma types from traces of intensional events
* completed …



@3096

7 years 
tranquil 
preliminary work on closing correctness.ma



@3072

7 years 
tranquil 
corrected a bug (translate_store was wrong)



@3037

7 years 
tranquil 
* ADDRESS joint instruction now has also an offset
* corrected call to …



@3018

7 years 
sacerdot 
1) some files repaired
2) all stuff related to the aborted pass …



@3014

7 years 
tranquil 
ERTL to ERTLptr pass suppressed (it introduced a bug in the later …



@2991

7 years 
piccolo 
Fixed cond and seq case in StatusSimulationHelper?
Added cost case in …



@2952

7 years 
tranquil 
* corrected all backend premains to not pass any arguments to the …



@2946

7 years 
tranquil 
main novelties:
* there is an inbuilt stack_usage nat in joint …



@2943

7 years 
sacerdot 
Mauro, I have put a daemon in place of the proof obligation that used …



@2942

7 years 
sacerdot 
Many changes:
1. Coloured graphs are now specified in terms of …



@2940

7 years 
sacerdot 
1. StatusSimulationHelper? changed to allow to use status_rel that …



@2898

7 years 
piccolo 
1) simplification of cond and seq case for StatusSimulationHelper? …



@2891

7 years 
piccolo 
added precondition on seq statement and tested correct in the …



@2883

7 years 
piccolo 
partial commit



@2868

7 years 
sacerdot 
Pretty printing of ERTL and ERTLptr code.



@2845

7 years 
piccolo 
ERTLptr to LTL correctness proof started



@2843

7 years 
piccolo 
1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof …



@2823

7 years 
tranquil 
* corrected bug in ERTL semantics (both delframe and newframe did the …



@2820

7 years 
sacerdot 
Proof obligation closed.



@2818

7 years 
sacerdot 
"Repaired", using non computational daemons.



@2807

7 years 
mckinna 
Yet another ErrorMessage?
Removed corresponding axiom in …



@2806

7 years 
tranquil 
new b_graph_translate obligations



@2801

7 years 
piccolo 
Partial commit not yet finished



@2796

7 years 
tranquil 
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …



@2786

7 years 
piccolo 
Splitted ERTLtoERTLptrOK.ma and added new file with commutation lemmas



@2785

7 years 
piccolo 
Traces.ma repaired



@2783

7 years 
piccolo 
modified joint_closed_internal_function definition (added condition on …



@2696

7 years 
sacerdot 
I can't get this right... :(



@2695

7 years 
sacerdot 
Renamed again.



@2693

7 years 
sacerdot 
1. Stuff moved to correct places.
2. ERTLptr pass added



@2691

7 years 
sacerdot 
ERTLtoERTLptr* moved to the proper place



@2689

7 years 
tranquil 
* fixed passes up to linearisation



@2681

7 years 
tranquil 
* improvements to the graph translation function
* fixed passes up to LTL



@2674

7 years 
tranquil 
* another change in block definition
* RTLabs > RTL and ERTL > …



@2666

7 years 
piccolo 
bug fixed in blocks.ma



@2645

7 years 
sacerdot 
1. some broken backend files repaires, several still to go
2. the …



@2604

7 years 
piccolo 
ERTLtoERTLptr in place.



@2601

7 years 
sacerdot 
Extraction to ocaml is now working, with a couple of bugs left.
One …



@2590

7 years 
piccolo 
added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc …



@2566

7 years 
piccolo 
ERTL to ERTLptr pass implemented up to a few things to be
left to the …



@2564

7 years 
piccolo 
ERTL fully repaired, useless part of return value of pop_ra
removed.



@2563

7 years 
piccolo 
Repairing ERTL: show stopper found.



@2490

7 years 
tranquil 
switched back to Byte immediate (instead of beval ones)
propagated …



@2443

7 years 
tranquil 
changed joint's stack pointer and internal stack



@2286

8 years 
tranquil 
Big update!
* merge of all _paolo variants
* reorganised some depends …



@2233

8 years 
tranquil 
* completed update of ERTL semantics
* some minor changes in joint …



@2217

8 years 
tranquil 
* collapsed step_params, unserialized_params, funct_params and …



@2214

8 years 
tranquil 
* changed order of parameters of joint_internal_function and genv in …



@2208

8 years 
tranquil 
* moving some code around
* changed immediates to hold beval in …



@2182

8 years 
tranquil 
updated linearisation pass



@2175

8 years 
tranquil 
corrected small bug



@2174

8 years 
tranquil 
* factored out script for (axiomatised) fixpoint computation
* ERTL → …



@2162

8 years 
tranquil 
* yet another correction to joint
* added functions adding prologues …



@2103

8 years 
campbell 
Make transform_*program take a more general transformation to make …



@2041

8 years 
sacerdot 
Repaired: unified syntax for monads.



@1995

8 years 
campbell 
Overall compiler definition; bits and pieces to
make everything happy(ish).



@1730

8 years 
sacerdot 
Minor changes while studying the proof.



@1729

8 years 
sacerdot 
Comment left from SVN merge removed.



@1601

8 years 
sacerdot 
Files ported to new version of the standard library.



@1515

8 years 
campbell 
Add type of maps on positive binary numbers, and use them for …



@1463

8 years 
mulligan 
added erasure for lin



@1451

8 years 
sacerdot 
1. All axioms in LIN/semantics.ma closed
2. succ_pc and …



@1429

8 years 
sacerdot 
Useless and removed.



@1425

8 years 
mulligan 
changes to the fixpoint calculation in ertl



@1424

8 years 
sacerdot 
1. fold function over BitVectorTries? moved from ERTLToLTL to …



@1423

8 years 
sacerdot 
 spill no longer used
 BUG IN Interference: generating the destruct …



@1415

8 years 
sacerdot 
1. hwreg_store/retrieve no longer returns a res (but it is still …



@1411

8 years 
sacerdot 
1. sem_params2 splitted into sem_params1 + sem_params2 to take out the …



@1408

8 years 
sacerdot 
1. Added joint/BEGlobalenvs that is a modification of …



@1390

8 years 
sacerdot 
All fetch_result implementations have been factorized out, leaving …



@1389

8 years 
sacerdot 
One more axiom closed.



@1388

8 years 
sacerdot 
fetch_result implemented for ERTL. This required a different …



@1386

8 years 
sacerdot 
Structure of semantic parameters simplified.



@1385

8 years 
sacerdot 
1. fetch_result and pop_frame now takes the genv in input
2. …



@1384

8 years 
sacerdot 
* fetch_ra taken out of pop_frame again since it is used uniformly and …



@1381

8 years 
sacerdot 
Old commented out code removed.



@1377

8 years 
sacerdot 
pop_frame now incorporates the fetch_result (that made sense only for …



@1372

8 years 
sacerdot 
save_frame now takes the stacksize to allow RTL to allocate the stack frame



@1371

8 years 
sacerdot 
save_frame changed to accept also the formal/actual argument pairs, …



@1359

8 years 
sacerdot 
1. more work on the RTL semantics
2. changes to joint/semantics to …



@1352

8 years 
sacerdot 
This commit is made necessary by the last Matita change.
Inclusion is …



@1329

8 years 
sacerdot 
1. Definition of addresses moved to BEMem
2. Basic functions on …



@1327

8 years 
sacerdot 
More progress in the implementation of the ERTL specific statements. …



@1324

8 years 
sacerdot 
The semantics of extended statements must also consider the label …



@1318

8 years 
sacerdot 
Frame management implemented.



@1313

8 years 
sacerdot 
(E)RTL semantics ported to new data type for save/pop frame (but not …



@1312

8 years 
sacerdot 
Type of frame operations (pop_frame/save_frame) generalized to take in …



@1303

8 years 
sacerdot 
1. LTL/semantics.ma added (work in progress)
2. init_locals fixed to …


