

@2453

8 years 
tranquil 
come changes in monad notation to
* avoid pretty printed monsters
* …



@2452

8 years 
piccolo 
Completed commutation lemmas of fetch_statement



@2450

8 years 
garnier 
Minor typo



@2449

8 years 
garnier 
Documentation added.



@2448

8 years 
garnier 
Comitting current state of switch removal.



@2447

8 years 
piccolo 
All axioms opened so far and that must be closed here have been
closed.



@2446

8 years 
piccolo 
Fetch commutation proof reduced to one simple (?) lemma.



@2445

8 years 
piccolo 
1. sigma function axiomatically defined (together with
its spec). …



@2444

8 years 
campbell 
Some inversion lemmas for after_n_steps for dealing with >1 source …



@2443

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



@2442

8 years 
piccolo 
Traces repaired. (By Paolo)
Statement of lineariseProof in place.



@2441

8 years 
garnier 
Moved general stuff on memories from switchRemoval to MemProperties?, …



@2440

8 years 
piccolo 
fixed range_strong and linearise
(commit by Paolo, he's to blame in case)



@2439

8 years 
campbell 
Get a proper reverse mapping of function blocks to identifiers by …



@2438

8 years 
garnier 
Sync of the w.i.p. for switch removal.



@2437

8 years 
tranquil 
generalised calls to calls with pointers



@2436

8 years 
tranquil 
small changes



@2435

8 years 
tranquil 
new back end operations



@2433

8 years 
campbell 
Tidy up Clight pointer comparison.



@2432

8 years 
campbell 
Remove offtheend pointers from front end ops.



@2429

8 years 
garnier 
Restrict semantics of pointer comparison to what CompCert? does  i.e. …



@2428

8 years 
campbell 
Tighten requirements on switch statements in Clight to only give …



@2426

8 years 
boender 
 updated stacksize to reflect new developments, completed proof
 …



@2423

8 years 
tranquil 
as_classifier predicate → as_classify function
as_call predicate from …



@2422

8 years 
tranquil 
adapted joint to cl_call f



@2421

8 years 
tranquil 
added simulation of flat prefix, and comments to explain the code



@2420

8 years 
campbell 
Tidy away generic results about folds on positive/identifier maps.



@2418

8 years 
campbell 
Add a checking function for the uniqueness of cost labels in RTLabs …



@2417

8 years 
boender 
 reverted changes to StructuredTraces? (shouldn't have been committed …



@2415

8 years 
campbell 
Add the ability to map blocks to symbols in preparation for stack space.



@2413

8 years 
tranquil 
* tal_rel corrected to include cases where tal_base_call \approx …



@2412

8 years 
campbell 
Tidy up measurable definition a bit more.



@2407

8 years 
campbell 
Sigh, continue in for loops was broken too.



@2399

8 years 
campbell 
Fill in some details about the statement of correctness.



@2398

8 years 
boender 
 committed start of stacksize



@2395

8 years 
campbell 
Proper handling of comparison of pointers offtheend of an object.
We …



@2393

8 years 
campbell 
A pointer comparison test case that illustrates a bug.



@2392

8 years 
campbell 
Labelling translations of && and  need a lot of cost labelling to …



@2391

8 years 
campbell 
Revert "Put the postloop cost label into the Clight while statement …



@2390

8 years 
campbell 
Tidy up a corner case when generating RTLabs so that we generate
less …



@2389

8 years 
campbell 
Fix dowhile statements, and carefully arrange the translation so that …



@2388

8 years 
campbell 
Example of each type of control flow statement, plus minor fix to …



@2387

8 years 
garnier 
Revamped memory extensions, proved stuff on freeing blocks and on …



@2386

8 years 
garnier 
Implementation of constructive finite sets based on lists. Various …



@2385

8 years 
campbell 
Minor housekeeping.



@2384

8 years 
campbell 
Move Matita pretty printers into place.



@2353

8 years 
campbell 
Put the postloop cost label into the Clight while statement to get …



@2338

8 years 
campbell 
Use much nicer definition for making several steps in the labelling …



@2335

8 years 
campbell 
Deal with goto labels in RTLabs to Cminor by fixing up goto statements …



@2332

8 years 
garnier 
Some progress on switch removal. Small fix in the definition of free, …



@2328

8 years 
campbell 
Cut down the notion of a Clight labelled state to those where we pick …



@2327

8 years 
mulligan 
Fixed typos in paper highlighted by referees. More substantial …



@2326

8 years 
campbell 
More accurate notion of labelled states in Clight.



@2325

8 years 
campbell 
Fill out some Clight bits and pieces in correctness.ma.



@2324

8 years 
tranquil 
semantics of blocks: function to produce trace from execution of …



@2323

8 years 
campbell 
Some correctness proof comments.



@2322

8 years 
campbell 
Today's correctness groupthink.



@2320

8 years 
campbell 
Update compiler and correctness with labelling changes.



@2319

8 years 
campbell 
Generate perprogram cost labels rather than perfunction ones, and …



@2318

8 years 
boender 
 now it compiles



@2317

8 years 
boender 
 small changes to make things compile



@2316

8 years 
boender 
 committed temporary version: true version has to wait until I …



@2315

8 years 
campbell 
Add some more commentary.



@2314

8 years 
campbell 
Move generic definitions from recent commit to appropriate places.



@2313

8 years 
campbell 
RTLabs cost checker correct.



@2312

8 years 
garnier 
Memory injections, to be revised



@2311

8 years 
garnier 
Some more cleaning of switchRemoval …



@2310

8 years 
garnier 
Moved a lemma from switchRemoval to positive.



@2309

8 years 
garnier 
Removed the superfluous xorb definition and move some basic properties …



@2308

8 years 
campbell 
More proof (and corrections) on cost checking.



@2307

8 years 
campbell 
Half the proofs for sound cost labelling check.



@2306

8 years 
campbell 
An insertion sort for testing purposes.



@2305

8 years 
campbell 
RTLabs cost spec checking function implemented (lacks proof, or much …



@2304

8 years 
garnier 
Strengthened proof of associativity of bitvector addition. Some more …



@2303

8 years 
campbell 
Some preliminary checking of cost labelling properties in RTLabs.



@2302

8 years 
garnier 
Finally proved associativity of addition on bitvectors. Rejoice.



@2301

8 years 
mulligan 
Trying to get the big proof working again



@2300

8 years 
campbell 
Cut out some dead ends and add some comments to the last commit.



@2299

8 years 
campbell 
Soundly labelled RTLabs structured traces are "unrepeating".



@2298

8 years 
garnier 
WIP: converting switch removal from Z to bitvectors. Does not compile, …



@2297

8 years 
campbell 
Nicer form of steps until cost label bound in RTLabs.



@2296

8 years 
campbell 
Tidy up some illplaced definitions.



@2295

8 years 
campbell 
Start on showing unrepeating property of RTLabs structured traces: …



@2294

8 years 
campbell 
Make RTLabs cost spec deterministic.



@2293

8 years 
campbell 
Add instruction pointer for call states in RTLabs.



@2292

8 years 
campbell 
More RTLabs invariants.



@2291

8 years 
campbell 
Disable switch removal in compiler.ma for now.



@2290

8 years 
campbell 
Remove jump tables from RTLabs > RTL.



@2289

8 years 
campbell 
Update alias



@2288

8 years 
campbell 
Remove jumptables from RTLabs. :(



@2287

8 years 
campbell 
RTLabs typing for loads and stores.



@2286

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



@2285

8 years 
sacerdot 
1. duplicated code erased
2. POP case finished up to lemmas on …



@2284

8 years 
sacerdot 
PUSH finished



@2283

8 years 
mulligan 
Work from today.



@2282

8 years 
sacerdot 
PUSH case almost finished



@2281

8 years 
sacerdot 
…



@2280

8 years 
sacerdot 
Proof repaired.



@2279

8 years 
sacerdot 
1. Bug fixed in the semantics of PUSH (no indirection performed)
2. …



@2278

8 years 
mulligan 
Half of JC case complete


