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)
@3363
7 years
boender
- renamed directory
(edit)
@3362
7 years
boender
- added some bits as per Claudio's mail - rewrote some small things - …
(edit)
@3361
7 years
sacerdot
15 pages version
Diff
Rev
Age
Author
Log Message
(edit)
@3354
7 years
boender
- one more
(edit)
@3353
7 years
boender
- addressed minor corrections by referees
(edit)
@3352
7 years
boender
- nicified formulas
Diff
Rev
Age
Author
Log Message
(edit)
@3342
7 years
boender
- completed reworking of proofs
(edit)
@3341
7 years
boender
- more notation stuff (still needs work!)
Diff
Rev
Age
Author
Log Message
(edit)
@3338
7 years
boender
- updated statement of main correctness statement (still needs work)
Diff
Rev
Age
Author
Log Message
(edit)
@3304
7 years
boender
- added 2012 reviews - updated affiliation
Diff
Rev
Age
Author
Log Message
(edit)
@3255
7 years
tranquil
* dropped newframe and delframe (to be integrated in calls and returns …
Diff
Rev
Age
Author
Log Message
(edit)
@3145
7 years
tranquil
* removed sigma types from traces of intensional events * completed …
Diff
Rev
Age
Author
Log Message
(edit)
@3112
7 years
tranquil
added invariant that costlabels are only assigned to NOPs (not proved …
Diff
Rev
Age
Author
Log Message
(edit)
@3104
7 years
sacerdot
Performance improvement.
(edit)
@3103
7 years
mckinna
Simplified "include" dependencies
(edit)
@3102
7 years
mckinna
Removed redundant refs to current_instruction0, which itself has been …
(edit)
@3101
7 years
mckinna
Removed redundant lemma execute_1_technical, which is covered by …
(edit)
@3100
7 years
mckinna
Removed redundant defn of current_instruction0, which only appears in …
(edit)
@3099
7 years
mckinna
Simplified preliminaries: inefficient_address_of_word_labels, and …
(edit)
@3098
7 years
sacerdot
Performance improvement.
(edit)
@3097
7 years
sacerdot
Performance improvement in policy computation.
(edit)
@3096
7 years
tranquil
preliminary work on closing correctness.ma
(edit)
@3095
7 years
sacerdot
Some performance improvement: an heavy computation was done again and …
Diff
Rev
Age
Author
Log Message
(edit)
@3082
7 years
mckinna
Tidying up: the long comment about preamble/renamed_symbols in the …
Diff
Rev
Age
Author
Log Message
(edit)
@3078
7 years
tranquil
fixed change of Mov
Diff
Rev
Age
Author
Log Message
(edit)
@3076
7 years
mckinna
simplified include dependencies
(edit)
@3075
7 years
mckinna
Apologies for late folding in of old changes which were left over from …
Diff
Rev
Age
Author
Log Message
(edit)
@3066
7 years
tranquil
* implemented get_arg_16 for ACC_DPTR * LINToASM is now agnostic as to …
(edit)
@3065
7 years
sacerdot
Efficiency of semantics of assembled improved: ticks_of was …
(edit)
@3064
7 years
sacerdot
Efficiency of the semantics of assembly improved by avoiding the …
Diff
Rev
Age
Author
Log Message
(edit)
@3062
7 years
sacerdot
Bug fixed in the semantics of Mov: the offset was ignored. Now all …
Diff
Rev
Age
Author
Log Message
(edit)
@3060
7 years
sacerdot
Bug fixed in the semantics of JMP. The bug was due to a bug in the …
Diff
Rev
Age
Author
Log Message
(edit)
@3057
7 years
tranquil
lookup of function identifiers was not corrected with sigma
(edit)
@3056
7 years
tranquil
fixed a merge gone wrong
Diff
Rev
Age
Author
Log Message
(edit)
@3051
7 years
tranquil
fixed order of global initialization in LINToASM. For the moment …
Diff
Rev
Age
Author
Log Message
(edit)
@3045
7 years
tranquil
fixed what made test3 fail. However it involves a different notion of …
Diff
Rev
Age
Author
Log Message
(edit)
@3039
7 years
tranquil
* merged and extended
MovSuccessor?
and Mov in one instruction (Mov dst …
Diff
Rev
Age
Author
Log Message
(edit)
@3034
7 years
sacerdot
Bug fixed: COST instructions are now assembled as NOP to prevent the …
(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
Note:
See
TracRevisionLog
for help on using the revision log.
Download in other formats:
RSS Feed
ChangeLog