

@3096

7 years 
tranquil 
preliminary work on closing correctness.ma



@3066

7 years 
tranquil 
* implemented get_arg_16 for ACC_DPTR
* LINToASM is now agnostic as to …



@3051

7 years 
tranquil 
fixed order of global initialization in LINToASM. For the moment …



@3045

7 years 
tranquil 
fixed what made test3 fail. However it involves a different notion of …



@3040

7 years 
tranquil 
fixed LINToASM



@3039

7 years 
tranquil 
* merged and extended MovSuccessor? and Mov in one instruction (Mov dst …



@3037

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



@3028

7 years 
sacerdot 
Bug fixed: 82 and 83 (intended to be the addresses of DPH/DPL) should …



@3023

7 years 
sacerdot 
Typo fixed. It made all GOTOs jump to random positions in the ASM code.



@3017

7 years 
sacerdot 
Repaired.



@3016

7 years 
tranquil 
fixed after previous commit



@3014

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



@2994

7 years 
sacerdot 
The LIN printer.



@2984

7 years 
tranquil 
better LINToASM initialization of globals (to be tested!)



@2978

7 years 
tranquil 
merged accidentally backtracked changes



@2976

7 years 
tranquil 
* a dangling trivial proof obligation is now closed



@2975

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



@2969

7 years 
sacerdot 
Dead axiom removed :)



@2963

7 years 
sacerdot 
Bug fixed: the premain for the final code is now
COST k1
…



@2956

7 years 
tranquil 
fixed LTL/LIN semantics



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



@2837

8 years 
tranquil 
* filled in evaluation of LTL/LIN's extended instrucitons



@2830

8 years 
sacerdot 
Added abstractions in front of cases daemon for code extraction.



@2783

8 years 
piccolo 
modified joint_closed_internal_function definition (added condition on …



@2767

8 years 
mckinna 
WARNING: BIG commit, which pushes code_size_opt check into …



@2763

8 years 
sacerdot 
All daemons in compiler.ma closed (i.e. proof obligations added
to the …



@2760

8 years 
sacerdot 
1. Many files repaired.
2. 3 new daemons: 2 in Assembly.ma, 1 in …



@2754

8 years 
sacerdot 
1. WARNING: I commented out one of James's function used in …



@2708

8 years 
tranquil 
fixed linearise and LINToASM
LINToASM has now correct transformation …



@2645

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



@2601

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



@2537

8 years 
tranquil 
rolled back changes on calls in joint. Now the save_frame parameter …



@2490

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



@2443

8 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



@2174

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



@1995

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



@1601

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



@1522

9 years 
mulligan 
changes to preamble and lin to asm pass, resolved conflict in interpret



@1520

9 years 
campbell 
Generate cost labels with correct type.



@1515

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



@1451

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



@1415

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



@1411

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



@1408

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



@1390

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



@1386

9 years 
sacerdot 
Structure of semantic parameters simplified.



@1385

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



@1384

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



@1383

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



@1382

9 years 
sacerdot 
 succ_pc generalized to return a res (necessary for LIN semantics)
 …



@1380

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



@1379

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



@1378

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



@1377

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



@1372

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



@1371

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



@1359

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



@1324

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



@1312

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



@1304

9 years 
sacerdot 
Work in progress.



@1282

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



@1281

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



@1275

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



@1270

9 years 
sacerdot 
Making RTL syntax an instance of Joint.



@1268

9 years 
sacerdot 
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …



@1264

9 years 
sacerdot 
Almost ported to new Joint syntax.



@1250

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



@1246

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



@1245

9 years 
sacerdot 
RTLtoERTL and LINToASM: porting to new Joint data type in progress. …



@1236

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



@1233

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



@1224

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



@1183

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



@1179

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



@1171

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



@1168

9 years 
sacerdot 
Joint statements parameterized over a record.



@1167

9 years 
mulligan 
…



@1166

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



@1164

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



@1163

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



@1161

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



@1149

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



@1132

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



@1112

9 years 
mulligan 
got lin > asm stuff working



@1110

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



@1108

9 years 
mulligan 
changes to get ertltoltli to compile



@1089

9 years 
mulligan 
more changes from earlier in the week



@1082

9 years 
mulligan 
work from today on ertl > ltl pass



@878

9 years 
campbell 
Removal of manually inserted record projections.



@757

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



@734

9 years 
mulligan 
Fixed lin2asm.



@733

9 years 
mulligan 
Fixed partial commit.



@723

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


