[721] | 1 | 29/03/2011: |
---|
| 2 | Label moved out of ASM.ma labelled_instruction datatype, as the Paris compiler |
---|
| 3 | can only produce at most one label per instruction emitted. |
---|
| 4 | |
---|
| 5 | Merged the LTL and LIN datatypes. |
---|
| 6 | |
---|
| 7 | Added comments to the ASM datatypes. |
---|
| 8 | |
---|
| 9 | Changed identifiers from bytes to words. |
---|
| 10 | |
---|
| 11 | Formalised missing Assembly.ma file. |
---|
[723] | 12 | |
---|
| 13 | 30/03/2011: |
---|
| 14 | Split translate_statements into two functions. |
---|
| 15 | |
---|
| 16 | Added a dependent type for the invariant that a LIN function body does not |
---|
| 17 | start with a label, and is not empty. |
---|
[730] | 18 | |
---|
| 19 | 01/04/2011: |
---|
| 20 | In retrospect: |
---|
| 21 | |
---|
| 22 | The Clight semantics are based on CompCert 1.6 rather than the prototype's; |
---|
| 23 | this also affects some of the common files. |
---|
| 24 | |
---|
| 25 | The identifiers are Words so that we can use BitVectorTries for maps. |
---|
| 26 | Similarly, integers are based on BitVectors rather than Coq-style binary |
---|
| 27 | integers + range proof. |
---|
| 28 | |
---|
| 29 | 8051 memory spaces are present, but are not (yet?) in the prototype. |
---|
| 30 | |
---|
| 31 | Dependent types are used to fix the number of arguments for addressing modes |
---|
| 32 | in RTLabs. |
---|
[739] | 33 | |
---|
| 34 | 04/04/2011: |
---|
| 35 | common/Identifiers.ma provides identifiers similar to atomSig in the |
---|
| 36 | prototype, except that we use the universe's name as a tag for the type of |
---|
| 37 | identifiers to provide some extra type safety. |
---|
[750] | 38 | |
---|
| 39 | 08/04/2011: |
---|
| 40 | Make return register optional in RTLabs |
---|
[773] | 41 | |
---|
| 42 | 26/04/2011: |
---|
| 43 | Remove register from RTLabs return statements because it ends up being |
---|
| 44 | redundant (we always use the register in the function record). |
---|
| 45 | |
---|
| 46 | The constants follow CompCert's rather than the prototype's with the result |
---|
| 47 | that they match up more closely with the addressing modes in RTLabs. |
---|
[774] | 48 | |
---|
| 49 | One of the front end operations for subtraction (subpp) appears to be missing |
---|
| 50 | from the prototype at present. |
---|
[816] | 51 | |
---|
| 52 | 19/05/2011: |
---|
| 53 | Dump Param var_type from the Clight to Cminor stage - we need to treat them |
---|
| 54 | like the other variables. |
---|
| 55 | |
---|
| 56 | Generate list of pointer variables from Clight types rather than |
---|
| 57 | recalculation. |
---|
| 58 | |
---|
| 59 | Drop signatures from function call statements in Cminor and RTLabs - they |
---|
| 60 | appear to be unused. |
---|
[1065] | 61 | |
---|
| 62 | 13/07/2011: [belatedly] |
---|
| 63 | Offsets haven't been abstracted in the front end. They might be later if it |
---|
| 64 | turns out to be useful in the proofs. (See the messages in the thread |
---|
| 65 | "32 and 16 bits integers support" from the 16th June 2011.) |
---|
| 66 | |
---|
| 67 | The integer cast operation in the front end doesn't take the operand size. |
---|
| 68 | In keeping with the other operations, we deduce it from the operand. |
---|
| 69 | The sizes of the results are always mentioned so that they can be evaluated |
---|
| 70 | without consulting the type information (although this is a somewhat |
---|
| 71 | arbitrary decision). |
---|
| 72 | |
---|
[1143] | 73 | 30/08/2011: [annotation] |
---|
| 74 | There is a mismatch between the capability of external functions in the |
---|
| 75 | OCaml and Matita code. In OCaml they can interact with the memory. In |
---|
| 76 | Matita (following old? CompCert) they cannot. Hence, in the semantics |
---|
| 77 | of intermediate languages from ERTL on, we need to recover the arguments |
---|
| 78 | for the function not only from the registers, but also from the stack. |
---|
[1198] | 79 | |
---|
| 80 | 08/09/2011: |
---|
| 81 | The Clight cast simplification algorithm is quite different to the prototype's: |
---|
| 82 | it only needs to do a simple pattern match per recursion and copes with deeper |
---|
| 83 | arithmetic expressions such as (char)((int)x + (int)y + (int)z). |
---|