Timeline



Oct 20, 2011:

4:21 PM Changeset [1432] by mulligan
finished d4.2 report
3:57 PM Changeset [1431] by sacerdot
Back-end todo (in Italian only, sorry...)
3:55 PM Changeset [1430] by sacerdot
Bug fixed: push/pop must work on the isp (now added). Note: the sp is …
3:55 PM Changeset [1429] by sacerdot
Useless and removed.
3:32 PM Changeset [1428] by mulligan
finished d4.3 report
3:07 PM Changeset [1427] by mulligan
more added to d4.3 report
2:08 PM Changeset [1426] by boender
removed axiom
11:12 AM Changeset [1425] by mulligan
changes to the fixpoint calculation in ertl

Oct 19, 2011:

7:17 PM Changeset [1424] by sacerdot
1. fold function over BitVectorTries? moved from ERTLToLTL to …
6:05 PM Changeset [1423] by sacerdot
- spill no longer used - BUG IN Interference: generating the destruct …
6:05 PM Changeset [1422] by tranquil
corrected a small bug
5:59 PM Changeset [1421] by tranquil
first draft of peeling optimization: * a framework for heuristics has …
5:50 PM Changeset [1420] by mulligan
more changes
5:25 PM Changeset [1419] by sacerdot
All axioms closed.
5:11 PM Changeset [1418] by mulligan
correct ratios for semantics calculated
5:10 PM Changeset [1417] by boender
- proved that jumps always increase - this should make termination easy
4:43 PM Changeset [1416] by sacerdot
Maps from hardware registers to beval now implemented in ASM/I8051 (in …
4:22 PM Changeset [1415] by sacerdot
1. hwreg_store/retrieve no longer returns a res (but it is still …
4:03 PM Changeset [1414] by mulligan
more added
2:54 PM Changeset [1413] by mulligan
a lot more added, including updated parameters based on csc's recent submit
2:22 PM Changeset [1412] by sacerdot
Tailcalls (via ids or pointers) to internal functions implemented. …
1:39 PM Changeset [1411] by sacerdot
1. sem_params2 splitted into sem_params1 + sem_params2 to take out the …
11:54 AM Changeset [1410] by campbell
Remove a few old workarounds.
11:30 AM Changeset [1409] by mulligan
added more to appendix discussing code
11:30 AM Changeset [1408] by sacerdot
1. Added joint/BEGlobalenvs that is a modification of …
11:17 AM Changeset [1407] by mulligan
almost finished

Oct 18, 2011:

4:25 PM Changeset [1406] by mulligan
a little more
4:19 PM Changeset [1405] by mulligan
yet more added. apparently there's more parameters than i ever …
3:39 PM Changeset [1404] by boender
- reworked + added - added an axiom to arithmetic, but should be provable
3:12 PM Changeset [1403] by mulligan
more added
1:30 PM Changeset [1402] by mulligan
more added
12:39 PM Changeset [1401] by ricciott
Changes concerning the new behavior of destruct.
12:14 PM Changeset [1400] by mulligan
more added on parameters
11:38 AM Changeset [1399] by mulligan
more work on parameters

Oct 17, 2011:

8:20 PM Changeset [1398] by mulligan
more work on parameters
6:37 PM Changeset [1397] by mulligan
more changes, talking about parameters
5:43 PM Changeset [1396] by sacerdot
Proof obligation closed.
5:41 PM Changeset [1395] by sacerdot
1) New versions of pointer_of_beval/beval_of_pointer with a stricter …
4:50 PM Changeset [1394] by mulligan
reconfiguring of tables, and recalculation of ratios
3:50 PM Changeset [1393] by boender
- added invariant for policy trie to assembly - change (syntax only) …
2:08 PM Changeset [1392] by tranquil
fiddling with Cminor: elimination of loops, blocks and exits
1:09 PM Changeset [1391] by mulligan
more added
11:43 AM Changeset [1390] by sacerdot
All fetch_result implementations have been factorized out, leaving …
11:23 AM Changeset [1389] by sacerdot
One more axiom closed.
10:54 AM Changeset [1388] by sacerdot
fetch_result implemented for ERTL. This required a different …
2:01 AM Changeset [1387] by sacerdot
Further simplification *params1 no longer used.
1:58 AM Changeset [1386] by sacerdot
Structure of semantic parameters simplified.
1:40 AM Changeset [1385] by sacerdot
1. fetch_result and pop_frame now takes the genv in input 2. …

Oct 16, 2011:

7:42 PM Changeset [1384] by sacerdot
* fetch_ra taken out of pop_frame again since it is used uniformly and …

Oct 15, 2011:

12:13 AM Changeset [1383] by sacerdot
Potential bug fixed and bug found: the way pointers and labels are put …

Oct 14, 2011:

10:50 PM Changeset [1382] by sacerdot
- succ_pc generalized to return a res (necessary for LIN semantics) - …
10:29 PM Changeset [1381] by sacerdot
Old commented out code removed.
10:25 PM Changeset [1380] by sacerdot
LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma. …
7:44 PM Changeset [1379] by sacerdot
Invariant on LIN code removed. In Paris it was decided that a simpler …
7:32 PM Changeset [1378] by sacerdot
New file LIN/joint_LTL_LIN.ma to factorize out the syntactic …
7:22 PM Changeset [1377] by sacerdot
pop_frame now incorporates the fetch_result (that made sense only for …
5:55 PM Changeset [1376] by sacerdot
Stack deallocation for RTL implemented in pop_frame.
5:43 PM Changeset [1375] by mulligan
changes, fixing typos etc
3:51 PM Changeset [1374] by mulligan
added note about cfgs
3:51 PM Changeset [1373] by mulligan
changes to file based on claudio's suggestions
2:48 PM Changeset [1372] by sacerdot
save_frame now takes the stacksize to allow RTL to allocate the stack frame
1:42 PM Changeset [1371] by sacerdot
save_frame changed to accept also the formal/actual argument pairs, …
10:56 AM Changeset [1370] by campbell
D3.3: Added a subsection on the SmallstepExec?.ma definitions, plus a …
10:56 AM Changeset [1369] by campbell
Put type information into front-end unary ops. Slight change to …

Oct 13, 2011:

6:11 PM Changeset [1368] by sacerdot
A bug in the clear tactic makes the previous (correct) commit wrong. …
5:48 PM Changeset [1367] by sacerdot
Proof improvement, still somehow a bit slow.
11:33 AM Changeset [1366] by mulligan
added connections with other languages to d4.3 report, also fixed …
11:30 AM Changeset [1365] by mulligan
changed description of task in 4.2 report. added outline and …
11:11 AM Changeset [1364] by mulligan
finished the report on d4.2. starting d4.3 report

Oct 12, 2011:

9:11 PM Changeset [1363] by boender
- done stuff with create_label_trie
5:54 PM Changeset [1362] by mulligan
d4-2 report almost complete
11:52 AM Changeset [1361] by mulligan
more changes
11:47 AM Changeset [1360] by mulligan
added more on use of dependent types, and also discussing the …

Oct 11, 2011:

6:00 PM Changeset [1359] by sacerdot
1. more work on the RTL semantics 2. changes to joint/semantics to …
5:48 PM Changeset [1358] by mulligan
got rtlabs to rtl compiling, foldi_strong needs examining
5:42 PM Changeset [1357] by tranquil
* changed implementation of constant indexings with extensible arrays …
5:33 PM Changeset [1356] by mulligan
deleted redundant directory. added outlines for both reports, and …
3:32 PM Changeset [1355] by sacerdot
monadic fold_lefti added
2:38 PM Changeset [1354] by sacerdot
One axiom closed.
12:45 PM Changeset [1353] by sacerdot
This commit is made necessary by the last Matita change. Inclusion is …
12:45 PM Changeset [1352] by sacerdot
This commit is made necessary by the last Matita change. Inclusion is …
12:24 PM Changeset [1351] by campbell
Tidy up some loose ends from the invariants branch merge.
2:27 AM Changeset [1350] by sacerdot
Porting to latest destruct tactic. Note: the tactics has a few …

Oct 10, 2011:

11:32 PM Changeset [1349] by tranquil
* work on LIN completed * small implementation of extensible arrays
10:40 PM Changeset [1348] by sacerdot
7:22 PM Changeset [1347] by campbell
Remove obsolete definitions.
6:18 PM Changeset [1346] by campbell
Minor corrections and a paragraph of context in the abstract to …
5:50 PM Changeset [1345] by tranquil
work on ERTL and LTL completed
5:47 PM Changeset [1344] by sacerdot
Ported to new destruct.
5:27 PM Changeset [1343] by mulligan
fixed some bugs in the translation
5:16 PM Changeset [1342] by sacerdot
The new auto is much more powerful.
4:38 PM Changeset [1341] by sacerdot
Empty directory removed.
4:34 PM Changeset [1340] by tranquil
work on RTLabs and RTL completed
4:10 PM Changeset [1339] by sacerdot
Automation is now stronger.
4:05 PM Changeset [1338] by sacerdot
Automation is now stronger.
4:03 PM Changeset [1337] by sacerdot
Automation is now stronger.
3:54 PM Changeset [1336] by sacerdot
Ported to new Matita destruct/inversion. One lemma fails at qed. …
3:54 PM Changeset [1335] by sacerdot
Ported to new Matita stdlib.
2:17 PM Changeset [1334] by tranquil
work on Cminor completed
12:53 PM Changeset [1333] by sacerdot
Avoid using the name of the construction of jmeq.
12:41 PM Changeset [1332] by campbell
Summation example updated (needs computational K).
10:21 AM Changeset [1331] by mulligan
some changes, but i now have two contradictory proof obligations.

Oct 7, 2011:

6:39 PM Changeset [1330] by campbell
Evict obsolete file.
6:19 PM Changeset [1329] by sacerdot
1. Definition of addresses moved to BEMem 2. Basic functions on …
5:47 PM Changeset [1328] by tranquil
* bug in ClightUtilities?.find_max_depth_lbld fixed * single-entry loop …
4:15 PM Changeset [1327] by sacerdot
More progress in the implementation of the ERTL specific statements. …
3:48 PM Changeset [1326] by sacerdot
Code improved (now it uses the high level functions from …
3:45 PM Changeset [1325] by mulligan
finished implementing the translate constant function
3:32 PM Changeset [1324] by sacerdot
The semantics of extended statements must also consider the label …
3:26 PM Changeset [1323] by campbell
Reduce number of notations for destructive let on pairs to one.
2:59 PM Changeset [1322] by sacerdot
address => stack_address
2:37 PM Changeset [1321] by sacerdot
No longer/never implemented files removed.
2:17 PM Changeset [1320] by sacerdot
Frame operations implemented.
1:48 PM Changeset [1319] by tranquil
indexing branch is compiling again: * clight interpreter updated * …
1:48 PM Changeset [1318] by sacerdot
Frame management implemented.
12:28 PM Changeset [1317] by campbell
Fix listings in D3.2/D3.3.
12:26 PM Changeset [1316] by campbell
Merge in id-lookup-branch to trunk.
11:12 AM Changeset [1315] by mulligan
another move for the same reason. got rtlabs > rtl compiling again by …
11:03 AM Changeset [1314] by mulligan
name changes so that bash tab completion actually works with some …

Oct 6, 2011:

10:55 PM Changeset [1313] by sacerdot
(E)RTL semantics ported to new data type for save/pop frame (but not …
10:35 PM Changeset [1312] by sacerdot
Type of frame operations (pop_frame/save_frame) generalized to take in …
6:45 PM Changeset [1311] by campbell
Merge trunk to invariants branch, sorting out the handling of …
6:31 PM Changeset [1310] by tranquil
* finished changes on annotator * implementing indexes in interpreter
6:09 PM Changeset [1309] by boender
- refounded JEP
5:27 PM Changeset [1308] by mulligan
changes to translate_cst
2:08 PM Changeset [1307] by mulligan
adding translate_cst
11:19 AM Changeset [1306] by mulligan
small changes to rtlabs. what axioms remain look hard to close. need …
11:07 AM Changeset [1305] by tranquil
added indexes to loop constructors. Branch does not compile atm
1:24 AM Changeset [1304] by sacerdot
Work in progress.
12:16 AM Changeset [1303] by sacerdot
1. LTL/semantics.ma added (work in progress) 2. init_locals fixed to …

Oct 5, 2011:

11:36 PM Changeset [1302] by sacerdot
ERTL/semantics.ma ported to joint/SemanticUtils (in progress)
11:35 PM Changeset [1301] by sacerdot
Axioms re-grouped according to their use.
10:43 PM Changeset [1300] by sacerdot
More (graph) axioms implemented. Look at the comments marked with XXX …
9:53 PM Changeset [1299] by sacerdot
Functions from RTL/semantics.ma generalized to work on every graph …
9:41 PM Changeset [1298] by sacerdot
- fetch_statement now takes in input the globalenv - fetch_statement …
6:04 PM Changeset [1297] by tranquil
changed representation of indexings to a nameless one implemented with …
5:53 PM Changeset [1296] by mulligan
changes
4:15 PM Changeset [1295] by sacerdot
More progress.
3:19 PM Changeset [1294] by sacerdot
RTL semantics: porting to joint semantics started.
2:47 PM Changeset [1293] by mulligan
finished rtl abs to rtl transformation subject to closing some axioms …
11:15 AM Changeset [1292] by mulligan
more added to rtlabs translation
10:20 AM Changeset [1291] by tranquil
Started branch of untrusted compiler with indexed labels * added …

Oct 4, 2011:

2:00 AM Changeset [1290] by sacerdot
One more function ported to new Joint.
1:57 AM Changeset [1289] by sacerdot
semantics ported to latest Joint version

Oct 3, 2011:

5:33 PM Changeset [1288] by mulligan
more added to rtlabs to rtl pass
4:55 PM Changeset [1287] by mulligan
about 3/4 of the way through rtlabs to rtl now
4:07 PM Changeset [1286] by mulligan
more changes to the rtl abs to rtl pass
3:08 PM Changeset [1285] by mulligan
more implementation on maps, final push to get rtl abs to rtl working
8:35 AM Changeset [1284] by sacerdot
Bugs fixed: fresh_label changes the label universe, but this was not …

Sep 30, 2011:

3:12 AM Changeset [1283] by sacerdot
Bad programming practice removed: change_label is no longer required …

Sep 28, 2011:

11:50 PM Changeset [1282] by sacerdot
Cosmetic change: names of joint statements/instructions shortened and …
11:08 PM Changeset [1281] by sacerdot
Porting of all transformation to the joint syntax practically …
2:43 AM Changeset [1280] by sacerdot
Some progress in the porting of RTLAbstoRTL to the joint syntax: 1) …
2:41 AM Changeset [1279] by sacerdot
Bug fixed in definition of ltb.

Sep 27, 2011:

9:57 AM Changeset [1278] by sacerdot
oppargs requires two more arguments. RTLtoERTL to be fixed since it …

Sep 26, 2011:

6:58 PM Changeset [1277] by campbell
Runtime functions and conclusion for D3.2.
6:14 PM Changeset [1276] by campbell
Support for replacing operations with runtime support functions in …
6:07 PM Changeset [1275] by sacerdot
RTL ported to joint syntax, but: 1. bug discovered: opaccs should …
5:58 PM Changeset [1274] by mulligan
starting removing axioms from adts and giving them proper implementations
5:57 PM Changeset [1273] by campbell
Remove generated file.
5:57 PM Changeset [1272] by campbell
Revert accidental commit.
4:24 PM Changeset [1271] by mulligan
finished, kind of
3:59 PM Changeset [1270] by sacerdot
Making RTL syntax an instance of Joint.
3:06 PM Changeset [1269] by sacerdot
Useless include removed.
2:52 PM Changeset [1268] by sacerdot
1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
12:41 PM Changeset [1267] by campbell
Other bits and pieces for D3.3.
12:09 PM Changeset [1266] by sacerdot
Added second projection.
11:29 AM Changeset [1265] by campbell
Revisions to D3.3.

Sep 23, 2011:

6:44 PM Changeset [1264] by sacerdot
Almost ported to new Joint syntax.
5:12 PM Changeset [1263] by mulligan
changes
4:40 PM Changeset [1262] by sacerdot
RTLtoERTL ported to the joint syntax for ERTL. Now it is time to port …
4:17 PM Changeset [1261] by campbell
More of D3.2.
3:04 PM Changeset [1260] by mulligan
commit for csc
11:49 AM Changeset [1259] by sacerdot
More progress towards new Joint data type.
1:47 AM Changeset [1258] by sacerdot
More progress towards porting to joint syntax.

Sep 22, 2011:

6:04 PM Changeset [1257] by sacerdot
More progress in porting to joint datatype.
6:03 PM Changeset [1256] by mulligan
changes: added a mapi for graphs
4:23 PM Changeset [1255] by sacerdot
Major mistake fixed: op1 and op2 were assuming the source and dest …
4:16 PM Changeset [1254] by sacerdot
More progress towards porting of RTLtoERTL to joint syntax.
2:57 PM Changeset [1253] by mulligan
uses.ma finished
2:49 PM Changeset [1252] by sacerdot
graph_params added to joint/Joint.ma, together with useful common …
2:29 PM Changeset [1251] by mulligan
changes to get things compiling again after yet another CSC rearrangement!
12:02 PM Changeset [1250] by sacerdot
1. Sigma types projections moved to utilities/extralib.ma 2. Extended …
11:41 AM Changeset [1249] by mulligan
changes to get everything to typecheck again
10:13 AM Changeset [1248] by mulligan
deleted files that do not compile in utilities, changed ertl.ma to use …
3:03 AM Changeset [1247] by sacerdot
Code (almost) ported to latest joint/Joint.ma datatype. I still need …
2:50 AM Changeset [1246] by sacerdot
Yet another change to Joint.ma to accomodate all passes. The concrete …

Sep 21, 2011:

10:22 PM Changeset [1245] by sacerdot
RTLtoERTL and LINToASM: porting to new Joint data type in progress. …
6:08 PM Changeset [1244] by campbell
Sort out Clight semantics equivalence proof for new SmallstepExec?.
5:53 PM Changeset [1243] by mulligan
small changes
5:35 PM Changeset [1242] by sacerdot
Some clean-up.
5:28 PM Changeset [1241] by mulligan
changes for claudio
5:24 PM Changeset [1240] by sacerdot
Ported to common definitions.
5:21 PM Changeset [1239] by sacerdot
RTLAbstoRTL ported to new datatypes. Note: RTL syntax/semantics is …
4:25 PM Changeset [1238] by campbell
Update Cminor and RTLabs to fit SmallstepExec? changes.
3:58 PM Changeset [1237] by sacerdot
Wrong commit repaired.
3:56 PM Changeset [1236] by sacerdot
LTLToLin.ma completed (up to a couple of daemons used to provide dead …
12:14 PM Changeset [1235] by campbell
Some basic material for D3.2, but not yet finished.
12:14 PM Changeset [1234] by campbell
Add (rather brief) draft of D3.3.
11:57 AM Changeset [1233] by sacerdot
1) Ported to Brian's new dependent type for fullexec 2) Universe level …
11:24 AM Changeset [1232] by mulligan
big changes: got what was implemented in the ertl to ltl pass type …

Sep 20, 2011:

7:11 PM Changeset [1231] by campbell
Change SmallstepExec? so that states can depend on global information. …
3:56 PM Changeset [1230] by mulligan
more changes
1:26 PM Changeset [1229] by mulligan
changes
Note: See TracTimeline for information about the timeline view.