Timeline



Dec 5, 2012:

7:20 PM Changeset [2535] by campbell
Add the trivial C program with check that there's a measurable subtrace.
7:20 PM Changeset [2534] by campbell
Tweak measurable definition to stop at the return from a function.
7:20 PM Changeset [2533] by campbell
Some fall out from removing floats.
6:57 PM Changeset [2532] by tranquil
added FCOND in LIN, and rewritten linearise so that it never adds a …
1:28 PM Changeset [2531] by mckinna
Trivial tweaks.

Dec 4, 2012:

6:29 PM Changeset [2530] by tranquil
temporary switch to cl_jump treated as cl_other fixed script for new …
6:16 PM Changeset [2529] by tranquil
rewritten function handling in joint swapped call_rel with ret_rel in …
9:05 AM Changeset [2528] by piccolo
added cases PUSH, C_ADDRESS and COPACCS

Dec 3, 2012:

6:22 PM Changeset [2527] by garnier
Progress on CL to CM.
5:48 PM Changeset [2526] by sacerdot
5:39 PM Changeset [2525] by sacerdot
4:41 PM Changeset [2524] by mulligan
Avoiding conflicts
4:30 PM Changeset [2523] by sacerdot
4:15 PM Changeset [2522] by sacerdot
Generic stuff moved to infrastructure.
4:10 PM Changeset [2521] by sacerdot
..
4:07 PM Changeset [2520] by sacerdot
Now it is nice!
12:29 PM Changeset [2519] by mulligan
To prevent conflicts
12:28 PM Changeset [2518] by sacerdot
11:51 AM Changeset [2517] by sacerdot

Dec 2, 2012:

5:45 PM Changeset [2516] by mckinna
removed typedefs; restored older versions; moved typedefs to …
5:20 PM Changeset [2515] by sacerdot
4:40 PM Changeset [2514] by sacerdot
All .ma files committed: some of them are just in-progress.

Dec 1, 2012:

9:01 PM Changeset [2513] by mckinna
Minor tweaks. Simplified dependencies again.
8:36 PM Changeset [2512] by mckinna
Simplified dependencies on ASM, to allow rollback to when …

Nov 30, 2012:

6:31 PM Changeset [2511] by campbell
Conjecture main Cminor/RTLabs simulation results. Add a few notes …
4:40 PM Changeset [2510] by garnier
Some progress on the Cl -> Cm front
1:15 PM Changeset [2509] by campbell
misc note

Nov 29, 2012:

8:12 PM Changeset [2508] by mckinna
more tweaks. compiler and correctness still build.
7:14 PM Changeset [2507] by piccolo
finished pop case in commutation eval_Seq_no_pc
6:38 PM Changeset [2506] by campbell
Use common definition of measurable.
3:37 PM Changeset [2505] by mckinna
Cleaned up compiler.ma; some refactoring/additional code needed in …
3:33 PM Changeset [2504] by mckinna
More refactoring to support the tidied up compiler.ma
3:32 PM Changeset [2503] by mckinna
tidied up, with new auxiliary defns, some refactoring, some code …
11:59 AM Changeset [2502] by campbell
Sketch a little about how measurable traces might work with RTLabs and …
10:12 AM Changeset [2501] by piccolo
working on lineariseProof. Not yet finished.

Nov 28, 2012:

5:57 PM Changeset [2500] by garnier
Continuing work on simulation in Clight/Cminor?
12:52 PM Changeset [2499] by campbell
Separate out the RTLabs abstract status record from the proofs about …

Nov 27, 2012:

6:01 PM Changeset [2498] by mckinna
Refactor: Typedefs object_code and costlabel_map lifted out from …
5:59 PM Changeset [2497] by mckinna
Simplified dependencies on ASM; knock-on from changes in ASM/*.ma
5:50 PM Changeset [2496] by garnier
Some tentative work on the simulation proof for expressions, in order …
5:17 PM Changeset [2495] by piccolo
continuing lineariseProof

Nov 26, 2012:

6:24 PM Changeset [2494] by mckinna
Removed BJC's axiomatisation of rtlabs_to_rtl, now that …
6:00 PM Changeset [2493] by mckinna
Change in cst_well_defd to fix previously broken defn of …
11:52 AM Changeset [2492] by campbell
Reduce axiomatisation in compiler.ma.
11:30 AM Changeset [2491] by tranquil
fixed wrt change of list member definition

Nov 25, 2012:

1:33 PM Changeset [2490] by tranquil
switched back to Byte immediate (instead of beval ones) propagated …

Nov 23, 2012:

5:28 PM Changeset [2489] by campbell
Conjecture some Clight/Cminor? simulation results.
4:29 PM Changeset [2488] by garnier
glitch fixed
3:47 PM Changeset [2487] by campbell
Set up "after_n_steps" to enforce an invariant on states.
12:18 PM Changeset [2486] by campbell
First go at a generalised version of measurable.
11:22 AM Changeset [2485] by campbell
Sketch of Clight/Cminor? callstate simulation

Nov 22, 2012:

6:40 PM Changeset [2484] by piccolo
fixed Traces and semantics added commutation record (not yet finished) …
5:05 PM Changeset [2483] by garnier
Memory injections for Clight to Cminor, partially axiomatized.
3:49 PM Changeset [2482] by campbell
Note about front-end simulations
10:09 AM HiPEAC13 edited by amadio
(diff)

Nov 21, 2012:

12:12 PM HiPEAC13 created by campbell

Nov 20, 2012:

6:40 PM Changeset [2481] by piccolo
corrected some inconsistencies fixed some of lineariseProof
6:39 PM Changeset [2480] by mulligan
Some more changes.
5:12 PM Changeset [2479] by mulligan
A small amount of rewriting as i didn't like the original introduction …
2:28 PM Changeset [2478] by tranquil
unified is_internal_function_of_program and is_internal_function
1:41 PM Changeset [2477] by tranquil
status_simulation reformulated definition of joint_classify split up …

Nov 19, 2012:

6:04 PM Changeset [2476] by piccolo
fixed commutation lemmas in lineariseProof started proof of main …
5:13 PM Changeset [2475] by campbell
Get compiler.ma and correctness.ma checking again. Note that the …
10:57 AM Changeset [2474] by tranquil
changed form of a statement

Nov 16, 2012:

6:59 PM Changeset [2473] by tranquil
put some generic stuff we need in the back end in extraGlobalenvs …
6:41 PM Changeset [2472] by campbell
Misc clight->cminor notes.
6:41 PM Changeset [2471] by campbell
Tame global environments a little.

Nov 15, 2012:

7:06 PM Changeset [2470] by tranquil
completely separated program counters from code pointers in joint …
6:33 PM Changeset [2469] by campbell
Fix up opaque type errors from recent changes.
6:12 PM Changeset [2468] by garnier
Floats are gone from the front-end. Some trace amount might remain in …
4:43 PM Changeset [2467] by piccolo
LINEARISE PROOF MODIFIED NOT YED FIXED

Nov 14, 2012:

7:17 PM Changeset [2466] by campbell
Show how global environments in clight to cminor pass match up.
7:17 PM Changeset [2465] by campbell
Remove obsolete comment (runtime functions should be implemented later …
5:38 PM Changeset [2464] by piccolo
adapted lineariseProof to new semantics
1:20 PM Changeset [2463] by tranquil
swapped back call_rel and ret_rel…
10:31 AM Changeset [2462] by tranquil
separated in back end values program counters from code pointers …

Nov 13, 2012:

7:06 PM Changeset [2461] by campbell
First cut of inductive structured traces diagrams.
6:30 PM Changeset [2460] by campbell
Rest of variable characterisation.
6:30 PM Changeset [2459] by campbell
Syntax update
11:38 AM Changeset [2458] by campbell
Clight to Cminor allocates stack variables to disjoint regions within …
11:30 AM Changeset [2457] by tranquil
rewritten function handling in joint swapped call_rel with ret_rel in …
11:28 AM Changeset [2456] by boender
- added simple proof

Nov 12, 2012:

4:39 PM Changeset [2455] by campbell
Dump rough notes on RTLabs structured traces existence proof.
4:39 PM Changeset [2454] by campbell
More misc notes on clight->cminor.
4:30 PM Changeset [2453] by tranquil
come changes in monad notation to * avoid pretty printed monsters * …
12:50 PM Changeset [2452] by piccolo
Completed commutation lemmas of fetch_statement

Nov 10, 2012:

5:31 PM Changeset [2451] by mulligan
Structured traces paper for Brian as per e-mail conversation yesterday.

Nov 9, 2012:

6:04 PM Changeset [2450] by garnier
Minor typo
6:01 PM Changeset [2449] by garnier
Documentation added.
4:38 PM Changeset [2448] by garnier
Comitting current state of switch removal.
4:01 PM Changeset [2447] by piccolo
All axioms opened so far and that must be closed here have been closed.
1:21 PM Changeset [2446] by piccolo
Fetch commutation proof reduced to one simple (?) lemma.
11:47 AM Changeset [2445] by piccolo
1. sigma function axiomatically defined (together with its spec). …

Nov 8, 2012:

6:47 PM Changeset [2444] by campbell
Some inversion lemmas for after_n_steps for dealing with >1 source …
2:27 PM Changeset [2443] by tranquil
changed joint's stack pointer and internal stack

Nov 7, 2012:

6:12 PM Changeset [2442] by piccolo
Traces repaired. (By Paolo) Statement of lineariseProof in place.
6:02 PM Changeset [2441] by garnier
Moved general stuff on memories from switchRemoval to MemProperties?, …
5:11 PM Changeset [2440] by piccolo
fixed range_strong and linearise (commit by Paolo, he's to blame in case)
4:42 PM Changeset [2439] by campbell
Get a proper reverse mapping of function blocks to identifiers by …
11:18 AM Changeset [2438] by garnier
Sync of the w.i.p. for switch removal.

Nov 6, 2012:

5:00 PM Changeset [2437] by tranquil
generalised calls to calls with pointers
4:13 PM Changeset [2436] by tranquil
small changes
4:12 PM Changeset [2435] by tranquil
new back end operations
4:04 PM Changeset [2434] by campbell
Misc notes.
4:02 PM Changeset [2433] by campbell
Tidy up Clight pointer comparison.
3:17 PM Changeset [2432] by campbell
Remove off-the-end pointers from front end ops.
1:15 PM Changeset [2431] by campbell
Fix in matita-out branch too.
1:13 PM Changeset [2430] by campbell
Fix casting for conditionals in CompCert?-derived C parser.
12:53 PM Changeset [2429] by garnier
Restrict semantics of pointer comparison to what CompCert? does - i.e. …
12:02 PM Changeset [2428] by campbell
Tighten requirements on switch statements in Clight to only give …

Nov 5, 2012:

11:14 AM Changeset [2427] by mulligan
More work on explanation.
Note: See TracTimeline for information about the timeline view.