

@3371

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



@3265

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



@3263

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



@3261

6 years 
piccolo 
reverted joint_semantics rtl_semantics and ltl_semantics



@3259

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



@3256

6 years 
tranquil 
fixed compilation



@3255

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



@3145

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



@3096

6 years 
tranquil 
preliminary work on closing correctness.ma



@3037

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



@2975

6 years 
tranquil 
* RTL premain fixed
* fixed bug in back end ops (subtracting to a …



@2958

6 years 
sacerdot 
Error message implemented.



@2955

6 years 
tranquil 
corrected stupid typo



@2952

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



@2946

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



@2935

6 years 
tranquil 
separation of RTL semantics in three different versions, and …



@2876

7 years 
tranquil 
corrected another endianess bug in joint_semantics. Switched some …



@2862

7 years 
sacerdot 
Repaired, a reverse was enough.



@2861

7 years 
mckinna 
PROVISIONAL commit:
Unintentional list reversal cause final step of …



@2860

7 years 
sacerdot 
RTL printing, core dumps ATM



@2823

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



@2806

7 years 
tranquil 
new b_graph_translate obligations



@2796

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



@2783

7 years 
piccolo 
modified joint_closed_internal_function definition (added condition on …



@2689

7 years 
tranquil 
* fixed passes up to linearisation



@2681

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



@2659

7 years 
sacerdot 
Tailcall elimination no longer necessary:
1. the backend is almost …



@2645

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



@2640

7 years 
tranquil 
updated RTL and RTLabs to RTL translation



@2601

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



@2490

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



@2286

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



@2233

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



@2217

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



@2214

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



@2208

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



@2186

7 years 
tranquil 
updated joint semantics



@2176

7 years 
campbell 
Remove memory spaces other than XData and Code; simplify pointers as a …



@2174

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



@2162

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



@2155

7 years 
tranquil 
updates to blocks and RTLabs to RTL translation (which sidesteps …



@2103

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



@2035

7 years 
sacerdot 
Fixed



@2032

7 years 
sacerdot 
!! BEWARE: major commit !!
1) [affects everybody]
split for …



@1999

7 years 
campbell 
Make backend use the main global envs.



@1995

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



@1882

7 years 
tranquil 
big update, alas incomplete:
joint changed a bit, and all BE languages …



@1644

8 years 
tranquil 
minor changes



@1643

8 years 
tranquil 
* some changes in everything
* separated extensions in sequential and …



@1641

8 years 
tranquil 
* semanticsUtils_paolo.ma contains code to generate both graph and …



@1640

8 years 
tranquil 
* finished fork of semantics.ma
* unification of Errors under the …



@1636

8 years 
tranquil 
* added coercions to arguments (in RTL) and notation for ops (for the …



@1635

8 years 
tranquil 
* lists with binders and monads
* Joint.ma and other temprarily …



@1601

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



@1516

8 years 
sacerdot 
Ported to syntax of Matita 0.99.1.



@1481

8 years 
sacerdot 
Proof fixed. The new standard library does not index any longer the …



@1451

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



@1450

8 years 
sacerdot 
Disambiguation problem avoided.



@1415

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



@1412

8 years 
sacerdot 
Tailcalls (via ids or pointers) to internal functions implemented. …



@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 …



@1396

8 years 
sacerdot 
Proof obligation closed.



@1390

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



@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 …



@1376

8 years 
sacerdot 
Stack deallocation for RTL implemented in pop_frame.



@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 …



@1348

8 years 
sacerdot 
…



@1326

8 years 
sacerdot 
Code improved (now it uses the high level functions from …



@1324

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



@1322

8 years 
sacerdot 
address => stack_address



@1320

8 years 
sacerdot 
Frame operations implemented.



@1315

8 years 
mulligan 
another move for the same reason. got rtlabs > rtl compiling again by …



@1313

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



@1303

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



@1301

8 years 
sacerdot 
Axioms regrouped according to their use.



@1300

8 years 
sacerdot 
More (graph) axioms implemented. Look at the comments marked with XXX …



@1299

8 years 
sacerdot 
Functions from RTL/semantics.ma generalized to work on every graph …



@1298

8 years 
sacerdot 
 fetch_statement now takes in input the globalenv
 fetch_statement …



@1295

8 years 
sacerdot 
More progress.



@1294

8 years 
sacerdot 
RTL semantics: porting to joint semantics started.



@1284

8 years 
sacerdot 
Bugs fixed: fresh_label changes the label universe, but this was not …



@1283

8 years 
sacerdot 
Bad programming practice removed: change_label is no longer required …



@1282

8 years 
sacerdot 
Cosmetic change: names of joint statements/instructions shortened and …



@1280

8 years 
sacerdot 
Some progress in the porting of RTLAbstoRTL to the joint syntax:
1) …



@1278

8 years 
sacerdot 
oppargs requires two more arguments. RTLtoERTL to be fixed since it …



@1275

8 years 
sacerdot 
RTL ported to joint syntax, but:
1. bug discovered: opaccs should …



@1270

8 years 
sacerdot 
Making RTL syntax an instance of Joint.



@1262

8 years 
sacerdot 
RTLtoERTL ported to the joint syntax for ERTL. Now it is time to port …



@1259

8 years 
sacerdot 
More progress towards new Joint data type.



@1258

8 years 
sacerdot 
More progress towards porting to joint syntax.



@1257

8 years 
sacerdot 
More progress in porting to joint datatype.


