Changeset 2767 for src


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
Files:
10 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
  • src/LIN/LINToASM.ma

    r2763 r2767  
     1include "utilities/BitVectorTrieSet.ma".
     2include "utilities/state.ma".
     3
    14include "ASM/Util.ma".
    2 include "utilities/BitVectorTrieSet.ma".
     5include "ASM/ASM.ma".
     6
    37include "LIN/LIN.ma".
    4 include "ASM/ASM.ma".
    5 include "utilities/state.ma".
    68
    79(* utilities to provide Identifier's and addresses  *)
     
    359361  〈u, foldi ??? f imap [ ]〉.
    360362
    361 definition lin_to_asm : lin_program → pseudo_assembly_program ≝
     363definition lin_to_asm : lin_program → option pseudo_assembly_program ≝
    362364  λp.
    363365  state_run ?? (new_ASM_universe p)
     
    370372     ! exit_label ← ASM_fresh … ;
    371373     ! main ← Identifier_of_ident … (prog_main … p) ;
    372      let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
    373374     ! symboltable ← get_symboltable … ;
    374      (* atm no data identifier is used in the code, so preamble must be empty *)
    375375     return
    376       (mk_pseudo_assembly_program [ ] code ? symboltable exit_label ? ?)).
     376      (let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
     377       ! code_ok ← code_size_opt code ; 
     378       (* atm no data identifier is used in the code, so preamble must be empty *)
     379       return
     380        (mk_pseudo_assembly_program [ ] code code_ok symboltable exit_label ? ?))).
    377381cases daemon
    378382qed.
  • src/common/AST.ma

    r2645 r2767  
    1919include "basics/types.ma".
    2020include "common/Integers.ma".
     21include "common/Identifiers.ma".
    2122include "ASM/Arithmetic.ma".
    22 include "common/Identifiers.ma".
    2323
    2424
  • src/common/CostLabel.ma

    r2703 r2767  
    1 include "common/AST.ma".
    2 include "ASM/BitVectorTrie.ma".
     1include "common/Identifiers.ma".
    32
    43definition costlabel ≝ identifier CostTag.
     4
     5definition costlabel_eq : ∀x,y:costlabel. (x=y) + (x≠y) ≝ identifier_eq ?.
    56
    67(* For use in importing programs in intermediate languages. *)
    78definition costlabel_of_nat : nat → costlabel ≝ identifier_of_nat ?.
    89
    9 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    10 (* Costlabel Maps: the other distinguished instance of BitVectorTrie.         *)
    11 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    12 
    13 definition costlabel_map ≝ BitVectorTrie costlabel 16 (* ADDRESS_WIDTH *).
    14 
    15 definition costlabel_map0 : costlabel_map ≝ Stub ….
    16 
    17 definition costlabel_map_injective ≝
    18   λcost_labels: costlabel_map.
    19     ∀pc, pc',l.
    20       lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
    21         pc = pc'.
    22        
  • src/common/LabelledObjects.ma

    r2133 r2767  
     1include "utilities/lists.ma".
    12include "common/Identifiers.ma".
    2 include "utilities/lists.ma".
     3
    34include alias "arithmetics/nat.ma".
    45
  • src/compiler.ma

    r2763 r2767  
    3232axiom colour_graph : coloured_graph_computer.
    3333
    34 definition back_end : RTLabs_program → pseudo_assembly_program ≝
     34definition back_end : RTLabs_program → res pseudo_assembly_program ≝
    3535λp.
    3636  let p ≝ rtlabs_to_rtl p in
     
    3939  let p ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *)
    4040  let p ≝ ltl_to_lin p in
    41           lin_to_asm p.
     41          opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p).
    4242
    4343include "ASM/Policy.ma".
     
    5252definition assembler : pseudo_assembly_program → res labelled_object_code ≝
    5353λp.
    54 (*  ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) ?(*(program_ok_opt ? list_instr)*); *)
    5554  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p);
    5655  let sigma ≝ λppc. \fst sigma_pol ppc in
     
    6059include "ASM/ASMCosts.ma".
    6160
    62 (*CSC: move the next definitions, e.g. in BitVectorTrie *)
    63 definition in_codomain: ∀A:Type[0].∀n:nat. BitVectorTrie A n → A → Prop ≝
    64  λA,n,m,a. ∃k:BitVector n. lookup_opt … k m = Some … a.
     61(*CSC: move the next definitions, e.g. in BitVectorTrie; JHM: done! *)
    6562
    66 definition strong_decidable: Prop → Type[0] ≝
    67  λP:Prop. P + ¬ P.
    68 
    69 lemma strong_decidable_in_codomain:
    70  ∀A:DeqSet.∀n:nat.∀m: BitVectorTrie A n.∀a:A.
    71   strong_decidable (in_codomain A n m a).
    72  #A #n #m elim m
    73  [ normalize #a' #a inversion (a' == a) #H
    74    [ %1 %{(VEmpty …)} >(\P H) %
    75    | %2 % * #_ #EQ destruct lapply (\Pf H) /2/ ]
    76  | -n #n #L #R #Hl #Hr #a
    77    cases (Hl a) -Hl [#K %1 cases K #k #H %{(false:::k)} <H % ] #Hl
    78    cases (Hr a) -Hr [#K %1 cases K #k #H %{(true:::k)}  <H % ] #Hr
    79    %2 % * #k cases (BitVector_Sn … k) ** #tl #EQ >EQ whd in ⊢ (??%? → ?);
    80    normalize nodelta whd in match (tail ???); #abs [ cases Hr | cases Hl ] /3/
    81  | #n #A %2 % * #x normalize #abs destruct ]
    82 qed.
    83 
    84 (* can now move this defn to ASM/ASMCosts.ma *)
    8563definition lift_cost_map_back_to_front :
    8664  ∀clight, code_memory, lbls.
     
    9775λp.
    9876  ! 〈init_cost,p',p〉 ← front_end p;
    99   let p ≝ back_end p in
    100     ! p ← assembler p;
     77  ! p ← back_end p;
     78  ! p ← assembler p;
    10179  let k ≝ ASM_cost_map p in
    10280  let k' ≝
  • src/utilities/extranat.ma

    r2670 r2767  
    11include "basics/types.ma".
    22include "arithmetics/nat.ma".
     3include "utilities/option.ma".
     4
     5(* JHM: here, for definiteness; used in ASM/ASM.ma *)
     6let rec nat_bound_opt (N:nat) (n:nat) : option (n < N) ≝
     7match N return λy. option (n < y) with
     8[ O ⇒ None ?
     9| S N' ⇒
     10    match n return λx. option (x < S N') with
     11    [ O ⇒ (return (lt_O_S ?))
     12    | S n' ⇒ (! prf ← nat_bound_opt N' n' ; return (le_S_S ?? prf))
     13    ]
     14].
    315
    416inductive nat_compared : nat → nat → Type[0] ≝
  • src/utilities/option.ma

    r1976 r2767  
    8383lemma opt_Exists_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_Exists A P o → opt_Exists ? Q o
    8484  ≝ m_pred_mp ….
     85 
     86(* moved from ASM/ASM.ma! *)
     87definition partial_injection : ∀A,B.(A → option B) → Prop ≝
     88λA,B,f.∀x,y,z.f x = Some ? z → f y = Some ? z → x = y.
Note: See TracChangeset for help on using the changeset viewer.