Changeset 2767 for src/ASM


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.

Location:
src/ASM
Files:
3 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
  • src/ASM/BitVectorTrie.ma

    r2028 r2767  
    710710  ]
    711711] qed.
     712
     713include "basics/deqsets.ma".
     714
     715definition in_codomain: ∀A:Type[0].∀n:nat. BitVectorTrie A n → A → Prop ≝
     716 λA,n,m,a. ∃k:BitVector n. lookup_opt … k m = Some … a.
     717
     718definition strong_decidable: Prop → Type[0] ≝
     719 λP:Prop. P + ¬ P.
     720
     721lemma strong_decidable_in_codomain:
     722 ∀A:DeqSet.∀n:nat.∀m: BitVectorTrie A n.∀a:A.
     723  strong_decidable (in_codomain A n m a).
     724 #A #n #m elim m
     725 [ normalize #a' #a inversion (a' == a) #H
     726   [ %1 %{(VEmpty …)} >(\P H) %
     727   | %2 % * #_ #EQ destruct lapply (\Pf H) /2/ ]
     728 | -n #n #L #R #Hl #Hr #a
     729   cases (Hl a) -Hl [#K %1 cases K #k #H %{(false:::k)} <H % ] #Hl
     730   cases (Hr a) -Hr [#K %1 cases K #k #H %{(true:::k)}  <H % ] #Hr
     731   %2 % * #k cases (BitVector_Sn … k) ** #tl #EQ >EQ whd in ⊢ (??%? → ?);
     732   normalize nodelta whd in match (tail ???); #abs [ cases Hr | cases Hl ] /3/
     733 | #n #A %2 % * #x normalize #abs destruct ]
     734qed.
     735
     736
  • src/ASM/CodeMemory.ma

    r2754 r2767  
    44(*include "ASM/UtilBranch.ma". *)
    55
     6include "utilities/option.ma".
     7
    68include alias "arithmetics/nat.ma".
     9
     10let rec nat_bound_opt (N:nat) (n:nat) : option (n < N) ≝
     11match N return λy. option (n < y) with
     12[ O ⇒ None ?
     13| S N' ⇒
     14    match n return λx. option (x < S N') with
     15    [ O ⇒ (return (lt_O_S ?))
     16    | S n' ⇒ (! prf ← nat_bounded N' n' ; return (le_S_S ?? prf))
     17    ]
     18].
     19
    720
    821(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    247260(* ***** Object-code ***** JHM: push elsewherein ASM/*.ma? *)
    248261
     262(*
    249263inductive nat_bounded : nat → nat → Type[0] ≝
    250264| nat_ok : ∀n,m:nat. nat_bounded n (n+m)
     
    270284  ]
    271285qed. 
    272 
    273 definition program_ok_opt : ∀A. ∀instrs : list A. option (program_size_ok (S(S(|instrs|))))
    274   ≝ λA.λinstrs. nat_bound_opt max_program_size (S(S(|instrs|))). (* for Policy.ma etc. *)
    275 
    276 
    277 
    278 
    279 
    280  
     286*)
     287
     288definition program_ok_opt : ∀A. ∀instrs : list A. option (program_size_ok (S(|instrs|)))
     289  ≝ λA.λinstrs. nat_bound_opt max_program_size (S(|instrs|)). (* for Policy.ma etc. *)
     290
Note: See TracChangeset for help on using the changeset viewer.