|
|
@2688
|
8 years |
tranquil |
* in Arithmeticcs.ma: commented include that breaks script in latest …
|
|
|
@2687
|
8 years |
tranquil |
* polished some interfaces
|
|
|
@2683
|
8 years |
tranquil |
proof of properties of b_graph_program_transform (with an open axiom)
|
|
|
@2681
|
8 years |
tranquil |
* improvements to the graph translation function
* fixed passes up to LTL
|
|
|
@2675
|
8 years |
tranquil |
* a generic graph program transformation
|
|
|
@2674
|
8 years |
tranquil |
* another change in block definition
* RTLabs -> RTL and ERTL -> …
|
|
|
@2666
|
8 years |
piccolo |
bug fixed in blocks.ma
|
|
|
@2661
|
8 years |
sacerdot |
stacksize "repaired" by "considering" tailcalls
Some daemons added …
|
|
|
@2655
|
8 years |
tranquil |
new step in code semantic lemma
|
|
|
@2647
|
8 years |
sacerdot |
Stupid typo fixed.
|
|
|
@2645
|
8 years |
sacerdot |
1. some broken back-end files repaires, several still to go
2. the …
|
|
|
@2642
|
8 years |
piccolo |
fixed joint/Traces after having posed block 0 to be Code
|
|
|
@2641
|
8 years |
piccolo |
defined dummy block code equals to 0
|
|
|
@2639
|
8 years |
sacerdot |
We are not going to prove erasure. Thus this becomes dead code.
|
|
|
@2638
|
8 years |
piccolo |
Back-end fixes for last Garnier's commit that removes the regions from …
|
|
|
@2601
|
8 years |
sacerdot |
Extraction to ocaml is now working, with a couple of bugs left.
One …
|
|
|
@2599
|
8 years |
tranquil |
* map_opt and map on positive maps are now clean (erase empty …
|
|
|
@2595
|
8 years |
tranquil |
* dropped locals and exit from definition of joint_if_function
* new …
|
|
|
@2592
|
8 years |
piccolo |
main lemma of ERTLptr in place
|
|
|
@2590
|
8 years |
piccolo |
added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc …
|
|
|
@2570
|
8 years |
piccolo |
ERTLtoERTLptr in place
|
|
|
@2564
|
8 years |
piccolo |
ERTL fully repaired, useless part of return value of pop_ra
removed.
|
|
|
@2562
|
8 years |
piccolo |
linearise modified
|
|
|
@2561
|
8 years |
tranquil |
* moved CALL as different case than joint_seq: lots of broken code now …
|
|
|
@2559
|
8 years |
piccolo |
lineariseProof finished
|
|
|
@2557
|
8 years |
tranquil |
minor modification of commented (for now) proof of correctness of …
|
|
|
@2556
|
8 years |
tranquil |
in joint semantics and traces: added a last popped calling address to …
|
|
|
@2555
|
8 years |
piccolo |
lemma eval_call_ok finished
|
|
|
@2553
|
8 years |
tranquil |
as_classify changed to a partial function
added a status for tailcalls
|
|
|
@2551
|
8 years |
piccolo |
completed isFinal and fetchStatementSigmaCommute. Fixed exit …
|
|
|
@2548
|
8 years |
tranquil |
in BackEndOps?, cleaner def of be_op2
new statement of …
|
|
|
@2547
|
8 years |
tranquil |
going on in proof of linearise
simplified by use of monadic functional …
|
|
|
@2543
|
8 years |
piccolo |
finished stmt_at_sigma_commute
|
|
|
@2538
|
8 years |
tranquil |
fixed Traces.ma after changes in joint/semantics.ma
|
|
|
@2537
|
8 years |
tranquil |
rolled back changes on calls in joint. Now the save_frame parameter …
|
|
|
@2536
|
8 years |
piccolo |
finished eval_seq_no_pc_sigma_commute lemma
|
|
|
@2532
|
8 years |
tranquil |
added FCOND in LIN, and rewritten linearise so that it never adds a …
|
|
|
@2529
|
8 years |
tranquil |
rewritten function handling in joint
swapped call_rel with ret_rel in …
|
|
|
@2528
|
8 years |
piccolo |
added cases PUSH, C_ADDRESS and COPACCS
|
|
|
@2507
|
8 years |
piccolo |
finished pop case in commutation eval_Seq_no_pc
|
|
|
@2501
|
8 years |
piccolo |
working on lineariseProof. Not yet finished.
|
|
|
@2495
|
8 years |
piccolo |
continuing lineariseProof
|
|
|
@2491
|
8 years |
tranquil |
fixed wrt change of list member definition
|
|
|
@2490
|
8 years |
tranquil |
switched back to Byte immediate (instead of beval ones)
propagated …
|
|
|
@2484
|
8 years |
piccolo |
fixed Traces and semantics
added commutation record (not yet finished) …
|
|
|
@2481
|
8 years |
piccolo |
corrected some inconsistencies
fixed some of lineariseProof
|
|
|
@2477
|
8 years |
tranquil |
status_simulation reformulated
definition of joint_classify split up …
|
|
|
@2476
|
8 years |
piccolo |
fixed commutation lemmas in lineariseProof
started proof of main …
|
|
|
@2474
|
8 years |
tranquil |
changed form of a statement
|
|
|
@2473
|
8 years |
tranquil |
put some generic stuff we need in the back end in extraGlobalenvs …
|
|
|
@2470
|
8 years |
tranquil |
completely separated program counters from code pointers in joint …
|
|
|
@2467
|
8 years |
piccolo |
LINEARISE PROOF MODIFIED NOT YED FIXED
|
|
|
@2464
|
8 years |
piccolo |
adapted lineariseProof to new semantics
|
|
|
@2462
|
8 years |
tranquil |
separated in back end values program counters from code pointers …
|
|
|
@2457
|
8 years |
tranquil |
rewritten function handling in joint
swapped call_rel with ret_rel in …
|
|
|
@2456
|
8 years |
boender |
- added simple proof
|
|
|
@2452
|
8 years |
piccolo |
Completed commutation lemmas of fetch_statement
|
|
|
@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). …
|
|
|
@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.
|
|
|
@2440
|
8 years |
piccolo |
fixed range_strong and linearise
(commit by Paolo, he's to blame in case)
|
|
|
@2437
|
8 years |
tranquil |
generalised calls to calls with pointers
|
|
|
@2426
|
8 years |
boender |
- updated stacksize to reflect new developments, completed proof
- …
|
|
|
@2422
|
8 years |
tranquil |
adapted joint to cl_call f
|
|
|
@2417
|
8 years |
boender |
- reverted changes to StructuredTraces? (shouldn't have been committed …
|
|
|
@2398
|
8 years |
boender |
- committed start of stacksize
|
|
|
@2324
|
8 years |
tranquil |
semantics of blocks: function to produce trace from execution of …
|
|
|
@2286
|
9 years |
tranquil |
Big update!
* merge of all _paolo variants
* reorganised some depends …
|
|
|
@2233
|
9 years |
tranquil |
* completed update of ERTL semantics
* some minor changes in joint …
|
|
|
@2217
|
9 years |
tranquil |
* collapsed step_params, unserialized_params, funct_params and …
|
|
|
@2214
|
9 years |
tranquil |
* changed order of parameters of joint_internal_function and genv in …
|
|
|
@2208
|
9 years |
tranquil |
* moving some code around
* changed immediates to hold beval in …
|
|
|
@2200
|
9 years |
tranquil |
* updated joint semantics: generation of linear and graph semantics
* …
|
|
|
@2186
|
9 years |
tranquil |
updated joint semantics
|
|
|
@2185
|
9 years |
campbell |
Use bitvectors for offsets.
|
|
|
@2182
|
9 years |
tranquil |
updated linearisation pass
|
|
|
@2176
|
9 years |
campbell |
Remove memory spaces other than XData and Code; simplify pointers as a …
|
|
|
@2162
|
9 years |
tranquil |
* yet another correction to joint
* added functions adding prologues …
|
|
|
@2155
|
9 years |
tranquil |
updates to blocks and RTLabs to RTL translation (which sidesteps …
|
|
|
@2103
|
9 years |
campbell |
Make transform_*program take a more general transformation to make …
|
|
|
@2043
|
9 years |
sacerdot |
Broken code commented out.
|
|
|
@2042
|
9 years |
sacerdot |
Repaired (Type => DeqSet?)
|
|
|
@1999
|
9 years |
campbell |
Make back-end use the main global envs.
|
|
|
@1995
|
9 years |
campbell |
Overall compiler definition; bits and pieces to
make everything happy(ish).
|
|
|
@1993
|
9 years |
campbell |
Make front-end memory model only depend on the general definitions by …
|
|
|
@1988
|
9 years |
campbell |
Abstraction of the memory contents in the memory models is no longer …
|
|
|
@1987
|
9 years |
campbell |
Move BEValues to common to reflect their use in the memory model for …
|
|
|
@1976
|
9 years |
tranquil |
* monads: just changed some defs, which had to be propagated in some …
|
|
|
@1949
|
9 years |
tranquil |
* lemma trace rel to eq flatten trace
* some more properties of …
|
|
|
@1908
|
9 years |
fguidi |
notation fixup following last commit of matita
we shifted the levels …
|
|
|
@1882
|
9 years |
tranquil |
big update, alas incomplete:
joint changed a bit, and all BE languages …
|
|
|
@1874
|
9 years |
campbell |
First cut at using back-end memory model throughout.
Note the …
|
|
|
@1709
|
9 years |
mulligan |
Changes to the execution of the MOVC instruction
|
|
|
@1644
|
9 years |
tranquil |
minor changes
|
|
|
@1643
|
9 years |
tranquil |
* some changes in everything
* separated extensions in sequential and …
|
|
|
@1641
|
9 years |
tranquil |
* semanticsUtils_paolo.ma contains code to generate both graph and …
|
|
|
@1640
|
9 years |
tranquil |
* finished fork of semantics.ma
* unification of Errors under the …
|
|
|
@1635
|
9 years |
tranquil |
* lists with binders and monads
* Joint.ma and other temprarily …
|
|
|