source: src/joint

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2476   7 years piccolo fixed commutation lemmas in lineariseProof started proof of main …
(edit) @2474   7 years tranquil changed form of a statement
(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) @2467   7 years piccolo LINEARISE PROOF MODIFIED NOT YED FIXED
(edit) @2464   7 years piccolo adapted lineariseProof to new semantics
(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) @2456   7 years boender - added simple proof
(edit) @2452   7 years piccolo Completed commutation lemmas of fetch_statement
(edit) @2447   7 years piccolo All axioms opened so far and that must be closed here have been closed.
(edit) @2446   7 years piccolo Fetch commutation proof reduced to one simple (?) lemma.
(edit) @2445   7 years piccolo 1. sigma function axiomatically defined (together with its spec). …
(edit) @2443   7 years tranquil changed joint's stack pointer and internal stack
(edit) @2442   7 years piccolo Traces repaired. (By Paolo) Statement of lineariseProof in place.
(edit) @2440   7 years piccolo fixed range_strong and linearise (commit by Paolo, he's to blame in case)
(edit) @2437   7 years tranquil generalised calls to calls with pointers
(edit) @2426   7 years boender - updated stacksize to reflect new developments, completed proof - …
(edit) @2422   7 years tranquil adapted joint to cl_call f
(edit) @2417   7 years boender - reverted changes to StructuredTraces? (shouldn't have been committed …
(edit) @2398   7 years boender - committed start of stacksize
(edit) @2324   7 years tranquil semantics of blocks: function to produce trace from execution of …
(edit) @2286   7 years tranquil Big update! * merge of all _paolo variants * reorganised some depends …
(edit) @2233   7 years tranquil * completed update of ERTL semantics * some minor changes in joint …
(edit) @2217   7 years tranquil * collapsed step_params, unserialized_params, funct_params and …
(edit) @2214   7 years tranquil * changed order of parameters of joint_internal_function and genv in …
(edit) @2208   7 years tranquil * moving some code around * changed immediates to hold beval in …
(edit) @2200   7 years tranquil * updated joint semantics: generation of linear and graph semantics * …
(edit) @2186   7 years tranquil updated joint semantics
(edit) @2185   7 years campbell Use bitvectors for offsets.
(edit) @2182   7 years tranquil updated linearisation pass
(edit) @2176   7 years campbell Remove memory spaces other than XData and Code; simplify pointers as a …
(edit) @2162   7 years tranquil * yet another correction to joint * added functions adding prologues …
(edit) @2155   7 years tranquil updates to blocks and RTLabs to RTL translation (which sidesteps …
(edit) @2103   7 years campbell Make transform_*program take a more general transformation to make …
(edit) @2043   8 years sacerdot Broken code commented out.
(edit) @2042   8 years sacerdot Repaired (Type => DeqSet?)
(edit) @1999   8 years campbell Make back-end use the main global envs.
(edit) @1995   8 years campbell Overall compiler definition; bits and pieces to make everything happy(ish).
(edit) @1993   8 years campbell Make front-end memory model only depend on the general definitions by …
(edit) @1988   8 years campbell Abstraction of the memory contents in the memory models is no longer …
(edit) @1987   8 years campbell Move BEValues to common to reflect their use in the memory model for …
(edit) @1976   8 years tranquil * monads: just changed some defs, which had to be propagated in some …
(edit) @1949   8 years tranquil * lemma trace rel to eq flatten trace * some more properties of …
(edit) @1908   8 years fguidi notation fixup following last commit of matita we shifted the levels …
(edit) @1882   8 years tranquil big update, alas incomplete: joint changed a bit, and all BE languages …
(edit) @1874   8 years campbell First cut at using back-end memory model throughout. Note the …
(edit) @1709   8 years mulligan Changes to the execution of the MOVC instruction
(edit) @1644   8 years tranquil minor changes
(edit) @1643   8 years tranquil * some changes in everything * separated extensions in sequential and …
(edit) @1641   8 years tranquil * semanticsUtils_paolo.ma contains code to generate both graph and …
(edit) @1640   8 years tranquil * finished fork of semantics.ma * unification of Errors under the …
(edit) @1635   8 years tranquil * lists with binders and monads * Joint.ma and other temprarily …
(edit) @1601   8 years sacerdot Files ported to new version of the standard library.
(edit) @1599   8 years sacerdot Start of merging of stuff into the standard library of Matita.
(edit) @1521   8 years sacerdot Syntax change in Matita: change what where => change where what.
(edit) @1516   8 years sacerdot Ported to syntax of Matita 0.99.1.
(edit) @1515   8 years campbell Add type of maps on positive binary numbers, and use them for …
(edit) @1472   8 years mulligan moved proof utils to erasure.ma
(edit) @1471   8 years mulligan finished erasure and generalised so as to work on arbitrary joint programs
(edit) @1470   8 years mulligan finished, pretty ugly though as matita's disambiguation is a …
(edit) @1469   8 years mulligan finished new relabelling for graphs subject to one axiom closed
(edit) @1467   8 years mulligan small change, adding entry and exit labels into the internal function, …
(edit) @1466   8 years mulligan erasure for graph based joint languages almost complete
(edit) @1463   8 years mulligan added erasure for lin
(edit) @1458   8 years mulligan added skeleton file for erasure function for joint languages
(edit) @1457   8 years sacerdot Bug fixed: when calling an internal function, the pc block is now set …
(edit) @1452   8 years sacerdot Bug fixed: labels MUST be represented as pointers whose block is the …
(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) @1419   8 years sacerdot All axioms closed.
(edit) @1416   8 years sacerdot Maps from hardware registers to beval now implemented in ASM/I8051 (in …
(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) @1380   8 years sacerdot LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma. …
(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) @1302   8 years sacerdot ERTL/semantics.ma ported to joint/SemanticUtils (in progress)
(edit) @1300   8 years sacerdot More (graph) axioms implemented. Look at the comments marked with XXX …
(edit) @1299   8 years sacerdot Functions from RTL/semantics.ma generalized to work on every graph …
(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
Note: See TracRevisionLog for help on using the revision log.