Search:
Login
Preferences
Help/Guide
About Trac
Wiki
Timeline
Roadmap
Browse Source
View Tickets
Search
Context Navigation
View Latest Revision
Older Revisions
→
source:
src
/
ASM
Revision Log Mode:
Stop on copy
Follow copies
Show only adds and deletes
View log starting at
and back to
Show at most
revisions per page.
Show full log messages
Legend:
Added
Modified
Copied or renamed
Diff
Rev
Age
Author
Log Message
(edit)
@3033
7 years
sacerdot
Bug fixed: sign_extension was extending according to the _second_ bit, …
Diff
Rev
Age
Author
Log Message
(edit)
@3028
7 years
sacerdot
Bug fixed: 82 and 83 (intended to be the addresses of DPH/DPL) should …
Diff
Rev
Age
Author
Log Message
(edit)
@3024
7 years
sacerdot
Bug fixed: set_flags was ignoring the cy and ov flags.
Diff
Rev
Age
Author
Log Message
(edit)
@2999
7 years
sacerdot
code_memory added to labelled_object_code to avoid recomputing it …
Diff
Rev
Age
Author
Log Message
(edit)
@2993
7 years
sacerdot
1. performance improved: the type inference was inferring …
Diff
Rev
Age
Author
Log Message
(edit)
@2910
7 years
sacerdot
Abstract statuses for ASM and OC completed. A simple test program can …
Diff
Rev
Age
Author
Log Message
(edit)
@2907
7 years
sacerdot
1. a few bugs fixed 2. as_return implemented for ASM & OC
(edit)
@2906
7 years
sacerdot
Bug fixed.
(edit)
@2905
7 years
sacerdot
Semantics of ASM in place (up to return values and function call …
Diff
Rev
Age
Author
Log Message
(edit)
@2899
7 years
sacerdot
1. some renaming ASM_xxx to OC_xxx 2. ASM_pre_classified_system …
Diff
Rev
Age
Author
Log Message
(edit)
@2875
7 years
sacerdot
Pretty printing of object code integrated too. A couple of axioms make …
Diff
Rev
Age
Author
Log Message
(edit)
@2832
7 years
sacerdot
Added abstraction in front of cases daemon for code extraction.
Diff
Rev
Age
Author
Log Message
(edit)
@2796
7 years
tranquil
* added global notation for existence in Type
[1]
(\exists
[1]
x.P) * in …
Diff
Rev
Age
Author
Log Message
(edit)
@2782
7 years
sacerdot
1. Paolo's bv_of_nat/nat_of_bv in
BitVector?
used to work with the …
(edit)
@2781
7 years
sacerdot
One more computational daemon closed.
Diff
Rev
Age
Author
Log Message
(edit)
@2771
7 years
sacerdot
Some speed up in Policy.ma.
(edit)
@2770
7 years
mckinna
WARNING: another big commit, touching many files in ASM/*.ma This …
Diff
Rev
Age
Author
Log Message
(edit)
@2767
7 years
mckinna
WARNING: BIG commit, which pushes code_size_opt check into …
Diff
Rev
Age
Author
Log Message
(edit)
@2764
7 years
sacerdot
preclassified_system for object code
(edit)
@2763
7 years
sacerdot
All daemons in compiler.ma closed (i.e. proof obligations added to the …
(edit)
@2762
7 years
sacerdot
All repaired up to compiler.ma. Note: one daemon is left for one …
(edit)
@2761
7 years
sacerdot
Unused (but not useless) code commented out.
(edit)
@2760
7 years
sacerdot
1. Many files repaired. 2. 3 new daemons: 2 in Assembly.ma, 1 in …
Diff
Rev
Age
Author
Log Message
(edit)
@2757
7 years
tranquil
many things are still broken, but there is a partial backtrack on …
(edit)
@2756
7 years
sacerdot
WARNING: this commit breaks things, sorry, Paolo is going to fix …
Diff
Rev
Age
Author
Log Message
(edit)
@2754
7 years
sacerdot
1. WARNING: I commented out one of James's function used in …
Diff
Rev
Age
Author
Log Message
(edit)
@2750
7 years
mckinna
Miscellany on 2
^{16 bounds, memory, lemmas+definitions. Completes …}
Diff
Rev
Age
Author
Log Message
(edit)
@2745
7 years
sacerdot
1. Complexity of policy computation lowered from O(n
^{2) to O(n) 2. …}
Diff
Rev
Age
Author
Log Message
(edit)
@2714
7 years
sacerdot
PolicyStep?
.ma repaired
(edit)
@2713
7 years
sacerdot
PolicyFront?
.ma repaired
Diff
Rev
Age
Author
Log Message
(edit)
@2710
7 years
sacerdot
ASMCosts.ma repaired
Diff
Rev
Age
Author
Log Message
(edit)
@2708
7 years
tranquil
fixed linearise and LINToASM LINToASM has now correct transformation …
(edit)
@2707
7 years
sacerdot
Assembly repaired.
Diff
Rev
Age
Author
Log Message
(edit)
@2705
7 years
sacerdot
More progress in ASM towards implementing the new pseudoinstructions.
(edit)
@2704
7 years
tranquil
moved JMP from instructions to preinstructions, and added
MovSuccessor?
…
Diff
Rev
Age
Author
Log Message
(edit)
@2702
7 years
sacerdot
1. proof closed in ASM/UtilBranch 2. more passes integrated in the …
Diff
Rev
Age
Author
Log Message
(edit)
@2700
7 years
sacerdot
1. exponential function dropped in favour of standard library 2. …
Diff
Rev
Age
Author
Log Message
(edit)
@2688
7 years
tranquil
* in Arithmeticcs.ma: commented include that breaks script in latest …
Diff
Rev
Age
Author
Log Message
(edit)
@2684
7 years
sacerdot
…
Diff
Rev
Age
Author
Log Message
(edit)
@2679
7 years
mckinna
Further tweak to Brian's changes: no normalization reqd at all!
Diff
Rev
Age
Author
Log Message
(edit)
@2676
7 years
campbell
Less aggressive normalisation in ASMCosts to prevent memory blowup.
Diff
Rev
Age
Author
Log Message
(edit)
@2673
7 years
tranquil
corrected some compilation errors (that might depend on some matita update)
(edit)
@2672
7 years
sacerdot
One less axiom on bitvectors.
(edit)
@2671
7 years
sacerdot
simplification
Diff
Rev
Age
Author
Log Message
(edit)
@2665
7 years
sacerdot
…
(edit)
@2664
7 years
sacerdot
Tailcall case implemented (it does not happen ATM).
Diff
Rev
Age
Author
Log Message
(edit)
@2657
7 years
sacerdot
Cost proof fully repaired. It was broken by the definitions used in …
(edit)
@2656
7 years
sacerdot
Ported to tailcalls (currently nothing is classified as a tailcall).
Diff
Rev
Age
Author
Log Message
(edit)
@2653
7 years
sacerdot
…
(edit)
@2652
7 years
sacerdot
String type changed definition.
(edit)
@2651
7 years
sacerdot
Type String changed.
Diff
Rev
Age
Author
Log Message
(edit)
@2647
7 years
sacerdot
Stupid typo fixed.
Diff
Rev
Age
Author
Log Message
(edit)
@2645
7 years
sacerdot
1. some broken back-end files repaires, several still to go 2. the …
Diff
Rev
Age
Author
Log Message
(edit)
@2643
7 years
sacerdot
We are not proving erasure, so this is dead code.
Diff
Rev
Age
Author
Log Message
(edit)
@2601
7 years
sacerdot
Extraction to ocaml is now working, with a couple of bugs left. One …
Diff
Rev
Age
Author
Log Message
(edit)
@2593
7 years
mckinna
Finally chased down wicked failure to close case 1.1: of …
Diff
Rev
Age
Author
Log Message
(edit)
@2575
7 years
mckinna
temporary commit localised the source of trouble in the proof of …
Diff
Rev
Age
Author
Log Message
(edit)
@2573
7 years
mckinna
temporary fixes to ensure {compiler,correctness}.ma recompile after …
Diff
Rev
Age
Author
Log Message
(edit)
@2531
7 years
mckinna
Trivial tweaks.
Diff
Rev
Age
Author
Log Message
(edit)
@2516
7 years
mckinna
removed typedefs; restored older versions; moved typedefs to …
Diff
Rev
Age
Author
Log Message
(edit)
@2508
7 years
mckinna
more tweaks. compiler and correctness still build.
Diff
Rev
Age
Author
Log Message
(edit)
@2504
7 years
mckinna
More refactoring to support the tidied up compiler.ma
Diff
Rev
Age
Author
Log Message
(edit)
@2498
7 years
mckinna
Refactor: Typedefs object_code and costlabel_map lifted out from …
Diff
Rev
Age
Author
Log Message
(edit)
@2475
7 years
campbell
Get compiler.ma and correctness.ma checking again. Note that the …
Diff
Rev
Age
Author
Log Message
(edit)
@2327
7 years
mulligan
Fixed typos in paper highlighted by referees. More substantial …
Diff
Rev
Age
Author
Log Message
(edit)
@2318
7 years
boender
- now it compiles
(edit)
@2317
7 years
boender
- small changes to make things compile
(edit)
@2316
7 years
boender
- committed temporary version: true version has to wait until I …
Diff
Rev
Age
Author
Log Message
(edit)
@2314
7 years
campbell
Move generic definitions from recent commit to appropriate places.
Diff
Rev
Age
Author
Log Message
(edit)
@2311
7 years
garnier
Some more cleaning of switchRemoval …
Diff
Rev
Age
Author
Log Message
(edit)
@2307
7 years
campbell
Half the proofs for sound cost labelling check.
Diff
Rev
Age
Author
Log Message
(edit)
@2301
7 years
mulligan
Trying to get the big proof working again
Diff
Rev
Age
Author
Log Message
(edit)
@2286
7 years
tranquil
Big update! * merge of all _paolo variants * reorganised some depends …
(edit)
@2285
7 years
sacerdot
1. duplicated code erased 2. POP case finished up to lemmas on …
(edit)
@2284
7 years
sacerdot
PUSH finished
(edit)
@2283
7 years
mulligan
Work from today.
(edit)
@2282
7 years
sacerdot
PUSH case almost finished
(edit)
@2281
7 years
sacerdot
…
(edit)
@2280
7 years
sacerdot
Proof repaired.
(edit)
@2279
7 years
sacerdot
1. Bug fixed in the semantics of PUSH (no indirection performed) 2. …
(edit)
@2278
7 years
mulligan
Half of JC case complete
Diff
Rev
Age
Author
Log Message
(edit)
@2276
7 years
sacerdot
…
(edit)
@2275
7 years
tranquil
* moved around some code (I8051.ma does not depend on
ByteValues?
.ma …
(edit)
@2274
7 years
sacerdot
Dead code commented out and code out of place moved to Test.ma.
(edit)
@2273
7 years
sacerdot
1. lemmas moved from all files to Test.ma 2. most of the lemmas in …
(edit)
@2272
7 years
mulligan
Changed proof strategy for main lemma after noticed that the current …
Diff
Rev
Age
Author
Log Message
(edit)
@2270
7 years
mulligan
Bug spotted and fixed in write_at_stack_pointer
(edit)
@2269
7 years
sacerdot
Proof completely repaired up to …
(edit)
@2268
7 years
mulligan
Bug spotted in instruction_size (lookup_datalabels cannot just be a …
(edit)
@2267
7 years
sacerdot
Call is now proved using the new strategy.
(edit)
@2266
7 years
sacerdot
All daemons closed in Jmp case.
(edit)
@2265
7 years
sacerdot
Commented out code removed.
(edit)
@2264
7 years
sacerdot
1) Major change: we now always use the efficient way of resolving …
Diff
Rev
Age
Author
Log Message
(edit)
@2262
7 years
mulligan
Changes from today.
(edit)
@2261
7 years
mulligan
Resolved conflict
(edit)
@2260
7 years
sacerdot
Now we use the efficient lookup_address.
(edit)
@2259
7 years
mulligan
For Claudio
(edit)
@2258
7 years
sacerdot
1. lemma generalized 2. automation replaced with expansion to make …
(edit)
@2257
7 years
mulligan
Daemon in SETB case closed.
(edit)
@2256
7 years
mulligan
MOV and MOVX cases complete
Note:
See
TracRevisionLog
for help on using the revision log.
Download in other formats:
RSS Feed
ChangeLog