source: src/joint/semantics.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2595   7 years tranquil * dropped locals and exit from definition of joint_if_function * new …
(edit) @2592   7 years piccolo main lemma of ERTLptr in place
(edit) @2590   7 years piccolo added monad machineary for ERTL to ERTLptr translation eval_seq_no_pc …
(edit) @2570   7 years piccolo ERTLtoERTLptr in place
(edit) @2564   7 years piccolo ERTL fully repaired, useless part of return value of pop_ra removed.
(edit) @2562   7 years piccolo linearise modified
(edit) @2561   7 years tranquil * moved CALL as different case than joint_seq: lots of broken code now …
(edit) @2556   7 years tranquil in joint semantics and traces: added a last popped calling address to …
(edit) @2551   7 years piccolo completed isFinal and fetchStatementSigmaCommute. Fixed exit …
(edit) @2537   7 years tranquil rolled back changes on calls in joint. Now the save_frame parameter …
(edit) @2532   7 years tranquil added FCOND in LIN, and rewritten linearise so that it never adds a …
(edit) @2529   7 years tranquil rewritten function handling in joint swapped call_rel with ret_rel in …
(edit) @2491   7 years tranquil fixed wrt change of list member definition
(edit) @2484   7 years piccolo fixed Traces and semantics added commutation record (not yet finished) …
(edit) @2481   7 years piccolo corrected some inconsistencies fixed some of lineariseProof
(edit) @2473   7 years tranquil put some generic stuff we need in the back end in extraGlobalenvs …
(edit) @2470   7 years tranquil completely separated program counters from code pointers in joint …
(edit) @2462   7 years tranquil separated in back end values program counters from code pointers …
(edit) @2457   7 years tranquil rewritten function handling in joint swapped call_rel with ret_rel in …
(edit) @2443   7 years tranquil changed joint's stack pointer and internal stack
(edit) @2437   7 years tranquil generalised calls to calls with pointers
(edit) @2422   7 years tranquil adapted joint to cl_call f
(edit) @2286   7 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
(edit) @2185   8 years campbell Use bitvectors for offsets.
(edit) @2176   8 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
(edit) @1999   8 years campbell Make back-end use the main global envs.
(edit) @1601   8 years sacerdot Files ported to new version of the standard library.
(edit) @1457   8 years sacerdot Bug fixed: when calling an internal function, the pc block is now set …
(edit) @1451   8 years sacerdot 1. All axioms in LIN/semantics.ma closed 2. succ_pc and …
(edit) @1430   8 years sacerdot Bug fixed: push/pop must work on the isp (now added). Note: the sp is …
(edit) @1415   8 years sacerdot 1. hwreg_store/retrieve no longer returns a res (but it is still …
(edit) @1411   8 years sacerdot 1. sem_params2 splitted into sem_params1 + sem_params2 to take out the …
(edit) @1408   8 years sacerdot 1. Added joint/BEGlobalenvs that is a modification of …
(edit) @1395   8 years sacerdot 1) New versions of pointer_of_beval/beval_of_pointer with a stricter …
(edit) @1390   8 years sacerdot All fetch_result implementations have been factorized out, leaving …
(edit) @1387   8 years sacerdot Further simplification *params1 no longer used.
(edit) @1386   8 years sacerdot Structure of semantic parameters simplified.
(edit) @1385   8 years sacerdot 1. fetch_result and pop_frame now takes the genv in input 2. …
(edit) @1384   8 years sacerdot * fetch_ra taken out of pop_frame again since it is used uniformly and …
(edit) @1383   8 years sacerdot Potential bug fixed and bug found: the way pointers and labels are put …
(edit) @1382   8 years sacerdot - succ_pc generalized to return a res (necessary for LIN semantics) - …
(edit) @1377   8 years sacerdot pop_frame now incorporates the fetch_result (that made sense only for …
(edit) @1376   8 years sacerdot Stack deallocation for RTL implemented in pop_frame.
(edit) @1372   8 years sacerdot save_frame now takes the stacksize to allow RTL to allocate the stack frame
(edit) @1371   8 years sacerdot save_frame changed to accept also the formal/actual argument pairs, …
(edit) @1359   8 years sacerdot 1. more work on the RTL semantics 2. changes to joint/semantics to …
(edit) @1352   8 years sacerdot This commit is made necessary by the last Matita change. Inclusion is …
(edit) @1329   8 years sacerdot 1. Definition of addresses moved to BEMem 2. Basic functions on …
(edit) @1324   8 years sacerdot The semantics of extended statements must also consider the label …
(edit) @1312   8 years sacerdot Type of frame operations (pop_frame/save_frame) generalized to take in …
(edit) @1303   8 years sacerdot 1. LTL/semantics.ma added (work in progress) 2. init_locals fixed to …
(edit) @1298   8 years sacerdot - fetch_statement now takes in input the globalenv - fetch_statement …
(edit) @1294   8 years sacerdot RTL semantics: porting to joint semantics started.
(edit) @1289   8 years sacerdot semantics ported to latest Joint version
(edit) @1281   8 years sacerdot Porting of all transformation to the joint syntax practically …
(edit) @1250   8 years sacerdot 1. Sigma types projections moved to utilities/extralib.ma 2. Extended …
(edit) @1247   8 years sacerdot Code (almost) ported to latest joint/Joint.ma datatype. I still need …
(edit) @1246   8 years sacerdot Yet another change to Joint.ma to accomodate all passes. The concrete …
(edit) @1233   8 years sacerdot 1) Ported to Brian's new dependent type for fullexec 2) Universe level …
(edit) @1220   8 years sacerdot ERTL ported to the new joint syntax.
(edit) @1217   8 years sacerdot Only one axiom left.
(edit) @1215   8 years sacerdot 1) Added shifting directly on pointers 2) More temporary axioms closed.
(edit) @1214   8 years sacerdot res_to_opt function added to common/Errors and used in joint/semantics …
(edit) @1213   8 years sacerdot 1) New values (joint/BEValues.ma) and memory model for the back-ends …
(edit) @1186   8 years sacerdot Spurious code removed. joint_fullexec implemented up to …
(edit) @1182   8 years mulligan changes to semantics: removing parameterised "next" element in joint …
(edit) @1177   8 years sacerdot Almost finished. Some functions still to be implemented, but I suspect …
(edit) @1176   8 years sacerdot
(edit) @1174   8 years sacerdot Semantics of most instructions completed.
(add) @1173   8 years sacerdot Unified semantics for ERTL/LTL/LIN (in progress). I hope to include …
Note: See TracRevisionLog for help on using the revision log.