source: src/joint

Revision Log Mode:


Legend:

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