

@3096

7 years 
tranquil 
preliminary work on closing correctness.ma



@3037

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



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



@2858

7 years 
sacerdot 
Trying to pretty print the code graph in visit order.
Slightly bugged …



@2848

7 years 
sacerdot 
The pretty printer for LTL.



@2845

7 years 
piccolo 
ERTLptr to LTL correctness proof started



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



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



@2443

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



@2286

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



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



@2205

8 years 
campbell 
Get correctness.ma type checking again.



@2182

8 years 
tranquil 
updated linearisation pass



@2174

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



@2103

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



@1515

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



@1451

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



@1383

8 years 
sacerdot 
Potential bug fixed and bug found: the way pointers and labels are put …



@1381

8 years 
sacerdot 
Old commented out code removed.



@1380

8 years 
sacerdot 
LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma. …



@1379

8 years 
sacerdot 
Invariant on LIN code removed. In Paris it was decided that a simpler …



@1378

8 years 
sacerdot 
New file LIN/joint_LTL_LIN.ma to factorize out the syntactic …



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



@1324

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



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



@1282

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



@1281

8 years 
sacerdot 
Porting of all transformation to the joint syntax practically …



@1280

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



@1271

8 years 
mulligan 
finished, kind of



@1270

8 years 
sacerdot 
Making RTL syntax an instance of Joint.



@1269

8 years 
sacerdot 
Useless include removed.



@1252

8 years 
sacerdot 
graph_params added to joint/Joint.ma, together with useful common …



@1250

8 years 
sacerdot 
1. Sigma types projections moved to utilities/extralib.ma
2. Extended …



@1246

8 years 
sacerdot 
Yet another change to Joint.ma to accomodate all passes.
The concrete …



@1236

8 years 
sacerdot 
LTLToLin.ma completed (up to a couple of daemons used to provide dead …



@1233

8 years 
sacerdot 
1) Ported to Brian's new dependent type for fullexec
2) Universe level …



@1224

8 years 
sacerdot 
Type of programs in common/AST made more dependent.
In particular, the …



@1222

8 years 
sacerdot 
LTL fully ported to the joint syntax.



@1183

8 years 
mulligan 
removed parameterised label types in the three lowest level languages



@1180

8 years 
mulligan 
lin to ltl pass complete



@1179

8 years 
mulligan 
changes to ertl, ltl and lin to use new notion of joint params. ertl …



@1171

8 years 
mulligan 
changes made on claudio's request: changed order of nesting in the …



@1168

8 years 
sacerdot 
Joint statements parameterized over a record.



@1166

8 years 
mulligan 
moved joint ltl lin files into their own directory. more changes to …



@1164

8 years 
mulligan 
ltl to lin working again, more changes to joint syntax



@1163

8 years 
mulligan 
even more streamlining and fixes to get things type checking



@1161

8 years 
mulligan 
changes from today: merged ertl, ltl and lin into one datatype to …



@1149

8 years 
mulligan 
changes to get everything type checking again after changing names of …



@1132

8 years 
mulligan 
reunified ltl and lin instruction type, removing lifting in ltl and …



@1111

8 years 
mulligan 
minor change: marked some possibly dodgy (and very complex) code



@1110

8 years 
mulligan 
changes to get ltl to lin pass to work properly



@1089

8 years 
mulligan 
more changes from earlier in the week



@1082

9 years 
mulligan 
work from today on ertl > ltl pass



@759

9 years 
mulligan 
More work on the RTL to ERTL pass.



@757

9 years 
mulligan 
Lots more fixing to get both front and backends using same conventions …



@753

9 years 
mulligan 
Work from today.



@733

9 years 
mulligan 
Fixed partial commit.



@728

9 years 
mulligan 
Changes from last two days.



@723

9 years 
mulligan 
Added dependent type internalising the invariant that LIN function …



@722

9 years 
mulligan 
Committing changes from today. Several files do not typecheck.



@716

9 years 
mulligan 
Finished translating LTL statements to LIN statements. Need to …



@715

9 years 
mulligan 
Restored rev from Util as it appears that list reversal is not a part …



@714

9 years 
mulligan 
Work on translation from LTL to LIN.



@713

9 years 
mulligan 
Commit of initial LTL files.
