Changeset 2757 for src/ASM


Ignore:
Timestamp:
Mar 1, 2013, 7:13:49 PM (7 years ago)
Author:
tranquil
Message:

many things are still broken, but there is a partial backtrack on Structured traces's execute

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2754 r2757  
    44include "common/LabelledObjects.ma".
    55include "joint/String.ma".
     6
     7(* move! *)
     8definition 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.
    610
    711definition Identifier ≝ identifier ASMTag.
     
    987991   The second associative list assigns to Identifiers meant to be entry points
    988992   of functions the name of the function (that lives in a different namespace) *)
    989 definition preamble ≝ list (Identifier × Word) × (list (Identifier × ident)).
     993
    990994definition assembly_program ≝ list instruction.
    991 definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
    992 
    993 definition object_code ≝ list Byte.
    994 definition costlabel_map ≝ BitVectorTrie costlabel 16.
    995 definition symboltable_type ≝ BitVectorTrie ident 16.
    996 definition labelled_object_code ≝ object_code × (costlabel_map × symboltable_type).
     995
     996definition fetch_pseudo_instruction:
     997 ∀code_mem:list labelled_instruction. ∀pc:Word.
     998  nat_of_bitvector … pc < |code_mem| → (pseudo_instruction × Word) ≝
     999  λcode_mem.
     1000  λpc: Word.
     1001  λpc_ok.
     1002    let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? pc) … code_mem pc_ok in
     1003    let new_pc ≝ add ? pc (bitvector_of_nat … 1) in
     1004      〈instr, new_pc〉.
     1005
     1006lemma snd_fetch_pseudo_instruction:
     1007 ∀l,ppc,ppc_ok. \snd (fetch_pseudo_instruction l ppc ppc_ok) = add ? ppc (bitvector_of_nat ? 1).
     1008 #l #ppc #ppc_ok whd in ⊢ (??(???%)?); @pair_elim
     1009 #lft #rgt #_ %
     1010qed.
     1011
     1012lemma fetch_pseudo_instruction_vsplit:
     1013 ∀instr_list,ppc,ppc_ok.
     1014  ∃pre,suff,lbl.
     1015   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
     1016#instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
     1017cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
     1018lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
     1019#EQ %{lbl0} @EQ
     1020qed.
     1021
     1022lemma fetch_pseudo_instruction_append:
     1023 ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.
     1024  let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
     1025  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
     1026  〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
     1027 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
     1028 cut (|l1| + nat_of_bitvector … ppc < 2^16)
     1029 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
     1030 -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
     1031 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     1032 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ]
     1033 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
     1034 #lbl #instr normalize nodelta >add_associative %
     1035qed.
    9971036
    9981037(* labels & instructions *)
     
    10191058  ].
    10201059
     1060definition 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
     1080definition 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
     1092definition asm_cost_label : ∀mem : list labelled_instruction.
     1093  (Σw : Word.nat_of_bitvector … w < |mem|) → option costlabel ≝
     1094λmem,w_prf.
     1095match \fst (fetch_pseudo_instruction mem w_prf (pi2 ?? w_prf)) with
     1096[ Cost c ⇒ Some ? c
     1097| _ ⇒ None ?
     1098].
     1099
     1100record pseudo_assembly_program : Type[0] ≝
     1101{ preamble : list (Identifier × Word)
     1102; code : list labelled_instruction
     1103; renamed_symbols : list (Identifier × ident)
     1104; final_index : Word
     1105(* properties *)
     1106; asm_injective_costlabels :
     1107  partial_injection … (asm_cost_label code)
     1108; well_labelled_p : is_well_labelled_p code
     1109}.
     1110
     1111definition object_code ≝ list Byte.
     1112definition costlabel_map ≝ BitVectorTrie costlabel 16.
     1113definition symboltable_type ≝ BitVectorTrie ident 16.
     1114record labelled_object_code : Type[0] ≝
     1115{ oc :> object_code
     1116; costlabels : costlabel_map
     1117; symboltable : symboltable_type
     1118; final_pc : Word
     1119(* properties *)
     1120; oc_injective_costlabels :
     1121  partial_injection … (λpc.lookup_opt … pc costlabels)
     1122}.
     1123
    10211124
    10221125(* If instruction i is a jump, then there will be something in the policy at
     
    10601163  ].
    10611164 
    1062 definition is_jump_to ≝
    1063   λx:pseudo_instruction.λd:Identifier.
    1064   match x with
    1065   [ Instruction i ⇒ match i with
    1066     [ JC j ⇒ d = j
    1067     | JNC j ⇒ d = j
    1068     | JZ j ⇒ d = j
    1069     | JNZ j ⇒ d = j
    1070     | JB _ j ⇒ d = j
    1071     | JNB _ j ⇒ d = j
    1072     | JBC _ j ⇒ d = j
    1073     | CJNE _ j ⇒ d = j
    1074     | DJNZ _ j ⇒ d = j
    1075     | _ ⇒ False
    1076     ]
    1077   | Call c ⇒ d = c
    1078   | Jmp j ⇒ d = j
    1079   | _ ⇒ False
    1080   ].
  • src/ASM/Status.ma

    r2754 r2757  
    10281028qed.
    10291029
    1030 definition fetch_pseudo_instruction:
    1031  ∀code_mem:list labelled_instruction. ∀pc:Word.
    1032   nat_of_bitvector … pc < |code_mem| → (pseudo_instruction × Word) ≝
    1033   λcode_mem.
    1034   λpc: Word.
    1035   λpc_ok.
    1036     let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? pc) … code_mem pc_ok in
    1037     let new_pc ≝ add ? pc (bitvector_of_nat … 1) in
    1038       〈instr, new_pc〉.
    1039 
    1040 lemma snd_fetch_pseudo_instruction:
    1041  ∀l,ppc,ppc_ok. \snd (fetch_pseudo_instruction l ppc ppc_ok) = add ? ppc (bitvector_of_nat ? 1).
    1042  #l #ppc #ppc_ok whd in ⊢ (??(???%)?); @pair_elim
    1043  #lft #rgt #_ %
    1044 qed.
    1045 
    1046 lemma fetch_pseudo_instruction_vsplit:
    1047  ∀instr_list,ppc,ppc_ok.
    1048   ∃pre,suff,lbl.
    1049    (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
    1050 #instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
    1051 cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
    1052 lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
    1053 #EQ %{lbl0} @EQ
    1054 qed.
    1055 
    1056 lemma fetch_pseudo_instruction_append:
    1057  ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.
    1058   let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
    1059   fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
    1060   〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
    1061  #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
    1062  cut (|l1| + nat_of_bitvector … ppc < 2^16)
    1063  [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
    1064  -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
    1065  >nat_of_bitvector_bitvector_of_nat_inverse try assumption
    1066  [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ]
    1067  #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
    1068  #lbl #instr normalize nodelta >add_associative %
    1069 qed.
    1070 
    1071 definition is_well_labelled_p ≝
    1072   λinstr_list.
    1073   ∀id: Identifier.
    1074   ∀ppc.
    1075   ∀ppc_ok.
    1076   ∀i.
    1077     \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) = i →
    1078       (instruction_has_label id i →
    1079         occurs_exactly_once ASMTag pseudo_instruction id instr_list) ∧
    1080       (is_jump_to i id →
    1081         occurs_exactly_once ASMTag pseudo_instruction id instr_list).
    1082 
    1083 definition construct_datalabels: preamble → ? ≝
    1084   λthe_preamble: preamble.
     1030definition construct_datalabels: list (Identifier × Word) → ? ≝
     1031  λthe_preamble.
    10851032    \fst (foldl ((identifier_map ASMTag Word) × Word) ? (
    10861033    λt. λpreamble.
     
    10891036      let 〈carry, sum〉 ≝ half_add … addr size in
    10901037        〈add ? ? datalabels name addr, sum〉)
    1091           〈empty_map …, zero 16〉 (\fst the_preamble)).
     1038          〈empty_map …, zero 16〉 (the_preamble)).
Note: See TracChangeset for help on using the changeset viewer.