Changeset 2767 for src/ASM/ASM.ma


Ignore:
Timestamp:
Mar 3, 2013, 2:03:58 PM (7 years ago)
Author:
mckinna
Message:

WARNING: BIG commit, which pushes code_size_opt check into LIN/LINToASM.ma
following CSC's comment on my previous partial commit
plus rolls all the miscellaneous code motion into the rest of the repo.

suggest REBUILD compiler.ma/correctness.ma from scratch.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2763 r2767  
    1 include "ASM/BitVector.ma".
    2 include "common/Identifiers.ma".
    31include "common/CostLabel.ma".
    42include "common/LabelledObjects.ma".
     3include "common/AST.ma".
    54include "joint/String.ma".
    6 
    7 (* move! *)
    8 definition partial_injection : ∀A,B.(A → option B) → Prop ≝
    9 λA,B,f.∀x,y,z.f x = Some ? z → f y = Some ? z → x = y.
     5include "ASM/BitVectorTrie.ma".
    106
    117definition Identifier ≝ identifier ASMTag.
     
    10581054  ].
    10591055
    1060 definition is_jump_to ≝
    1061   λx:pseudo_instruction.λd:Identifier.
    1062   match x with
    1063   [ Instruction i ⇒ match i with
    1064     [ JC j ⇒ d = j
    1065     | JNC j ⇒ d = j
    1066     | JZ j ⇒ d = j
    1067     | JNZ j ⇒ d = j
    1068     | JB _ j ⇒ d = j
    1069     | JNB _ j ⇒ d = j
    1070     | JBC _ j ⇒ d = j
    1071     | CJNE _ j ⇒ d = j
    1072     | DJNZ _ j ⇒ d = j
    1073     | _ ⇒ False
    1074     ]
    1075   | Call c ⇒ d = c
    1076   | Jmp j ⇒ d = j
    1077   | _ ⇒ False
    1078   ].
    1079 
    1080 definition is_well_labelled_p ≝
    1081   λinstr_list.
    1082   ∀id: Identifier.
    1083   ∀ppc.
    1084   ∀ppc_ok.
    1085   ∀i.
    1086     \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) = i →
    1087       (instruction_has_label id i →
    1088         occurs_exactly_once ASMTag pseudo_instruction id instr_list) ∧
    1089       (is_jump_to i id →
    1090         occurs_exactly_once ASMTag pseudo_instruction id instr_list).
    1091 
    1092 definition asm_cost_label : ∀mem : list labelled_instruction.
    1093   (Σw : Word.nat_of_bitvector … w < |mem|) → option costlabel ≝
    1094 λmem,w_prf.
    1095 match \fst (fetch_pseudo_instruction mem w_prf (pi2 ?? w_prf)) with
    1096 [ Cost c ⇒ Some ? c
    1097 | _ ⇒ None ?
    1098 ].
    1099 
    1100 record pseudo_assembly_program : Type[0] ≝
    1101 { preamble : list (Identifier × Word)
    1102 ; code : list labelled_instruction
    1103 ; code_size_ok: S (|code|) < 2^16
    1104 ; renamed_symbols : list (Identifier × ident)
    1105 ; final_label : Identifier
    1106 (* properties *)
    1107 ; asm_injective_costlabels :
    1108   partial_injection … (asm_cost_label code)
    1109 ; well_labelled_p : is_well_labelled_p code
    1110 }.
    1111 
    1112 definition object_code ≝ list Byte.
    1113 definition costlabel_map ≝ BitVectorTrie costlabel 16.
    1114 definition symboltable_type ≝ BitVectorTrie ident 16.
    1115 record labelled_object_code : Type[0] ≝
    1116 { oc : object_code
    1117 ; costlabels : costlabel_map
    1118 ; symboltable : symboltable_type
    1119 ; final_pc : Word
    1120 (* properties *)
    1121 ; oc_injective_costlabels :
    1122   partial_injection … (λpc.lookup_opt … pc costlabels)
    1123 }.
    1124 
    1125 
    11261056(* If instruction i is a jump, then there will be something in the policy at
    11271057 * position i *)
     
    11641094  ].
    11651095 
     1096definition is_jump_to ≝
     1097  λx:pseudo_instruction.λd:Identifier.
     1098  match x with
     1099  [ Instruction i ⇒ match i with
     1100    [ JC j ⇒ d = j
     1101    | JNC j ⇒ d = j
     1102    | JZ j ⇒ d = j
     1103    | JNZ j ⇒ d = j
     1104    | JB _ j ⇒ d = j
     1105    | JNB _ j ⇒ d = j
     1106    | JBC _ j ⇒ d = j
     1107    | CJNE _ j ⇒ d = j
     1108    | DJNZ _ j ⇒ d = j
     1109    | _ ⇒ False
     1110    ]
     1111  | Call c ⇒ d = c
     1112  | Jmp j ⇒ d = j
     1113  | _ ⇒ False
     1114  ].
     1115
     1116definition is_well_labelled_p ≝
     1117  λinstr_list.
     1118  ∀id: Identifier.
     1119  ∀ppc.
     1120  ∀ppc_ok.
     1121  ∀i.
     1122    \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) = i →
     1123      (instruction_has_label id i →
     1124        occurs_exactly_once ASMTag pseudo_instruction id instr_list) ∧
     1125      (is_jump_to i id →
     1126        occurs_exactly_once ASMTag pseudo_instruction id instr_list).
     1127
     1128definition asm_cost_label : ∀mem : list labelled_instruction.
     1129  (Σw : Word.nat_of_bitvector … w < |mem|) → option costlabel ≝
     1130λmem,w_prf.
     1131match \fst (fetch_pseudo_instruction mem w_prf (pi2 ?? w_prf)) with
     1132[ Cost c ⇒ Some ? c
     1133| _ ⇒ None ?
     1134].
     1135
     1136(* XXX JHM: avoid magic numbers! *)
     1137definition ADDRESS_WIDTH ≝ 16.
     1138definition MAX_CODE_SIZE ≝ 2^ADDRESS_WIDTH.
     1139
     1140definition code_size_p : list labelled_instruction → Prop ≝
     1141  λcode. S (|code|) < MAX_CODE_SIZE.
     1142 
     1143definition code_size_opt : ∀code. option (code_size_p code) ≝
     1144  λcode. nat_bound_opt MAX_CODE_SIZE (S (|code|)).
     1145
     1146record pseudo_assembly_program : Type[0] ≝
     1147{ preamble : list (Identifier × Word)
     1148; code : list labelled_instruction
     1149; code_size_ok: code_size_p code
     1150; renamed_symbols : list (Identifier × ident)
     1151; final_label : Identifier
     1152(* properties *)
     1153; asm_injective_costlabels :
     1154  partial_injection … (asm_cost_label code)
     1155; well_labelled_p : is_well_labelled_p code
     1156}.
     1157
     1158definition object_code ≝ list Byte.
     1159definition costlabel_map ≝ BitVectorTrie costlabel 16. (* XXX *)
     1160definition symboltable_type ≝ BitVectorTrie ident 16.  (* XXX *)
     1161record labelled_object_code : Type[0] ≝
     1162{ oc : object_code
     1163; costlabels : costlabel_map
     1164; symboltable : symboltable_type
     1165; final_pc : Word
     1166(* properties *)
     1167; oc_injective_costlabels :
     1168  partial_injection … (λpc.lookup_opt … pc costlabels)
     1169}.
     1170
     1171
     1172
Note: See TracChangeset for help on using the changeset viewer.