Changeset 938


Ignore:
Timestamp:
Jun 10, 2011, 6:36:55 PM (8 years ago)
Author:
sacerdot
Message:

...

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r922 r938  
    202202                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
    203203                  [ DATA16 w ⇒ λ_.
    204                      let 〈b1,b2〉 ≝ split ? 8 8 w in
     204                     let b1_b2 ≝ split ? 8 8 w in
     205                     let b1 ≝ \fst b1_b2 in
     206                     let b2 ≝ \fst b1_b2 in
    205207                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
    206208                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
     
    352354     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    353355      [ ADDR11 w ⇒ λ_.
    354          let 〈v1,v2〉 ≝ split ? 3 8 w in
     356         let v1_v2 ≝ split ? 3 8 w in
     357         let v1 ≝ \fst v1_v2 in
     358         let v2 ≝ \snd v1_v2 in
    355359          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
    356360      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     
    358362     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    359363      [ ADDR11 w ⇒ λ_.
    360          let 〈v1,v2〉 ≝ split ?  3 8 w in
     364         let v1_v2 ≝ split ? 3 8 w in
     365         let v1 ≝ \fst v1_v2 in
     366         let v2 ≝ \snd v1_v2 in
    361367          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
    362368      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     
    366372     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    367373      [ ADDR16 w ⇒ λ_.
    368          let 〈b1,b2〉 ≝ split ? 8 8 w in
     374         let b1_b2 ≝ split ? 8 8 w in
     375         let b1 ≝ \fst b1_b2 in
     376         let b2 ≝ \snd b1_b2 in
    369377          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
    370378      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     
    372380     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    373381      [ ADDR16 w ⇒ λ_.
    374          let 〈b1,b2〉 ≝ split ? 8 8 w in
     382         let b1_b2 ≝ split ? 8 8 w in
     383         let b1 ≝ \fst b1_b2 in
     384         let b2 ≝ \snd b1_b2 in
    375385          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
    376386      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  • src/ASM/AssemblyProof.ma

    r937 r938  
    17611761    | Comment comment ⇒ 〈0, 0〉
    17621762    | Cost cost ⇒ 〈0, 0〉
    1763     | Jmp jmp ⇒ 〈0, 2〉
    1764     | Call call ⇒ 〈0, 2〉
    1765     | Mov dptr tgt ⇒ 〈0, 2〉
     1763    | Jmp jmp ⇒ 〈2, 2〉
     1764    | Call call ⇒ 〈2, 2〉
     1765    | Mov dptr tgt ⇒ 〈2, 2〉
    17661766    ].
    17671767  cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
     
    19841984    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    19851985    #H2 >(eq_bv_to_eq … H2) >EQ %
    1986   |4: (* Jmp *)
     1986  |4: (* Jmp *) #label
     1987      whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
     1988       [3: (* long *) #H1 #H2 #EQ %[@1]
     1989           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     1990           change in ⊢ (? → ??%?) with (execute_1_0 ??)
     1991           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     1992           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
     1993           >H2b >(eq_instruction_to_eq … H2a)
     1994           generalize in match EQ; -EQ;
     1995           (*whd in ⊢ (???% → ??%?);*)
     1996           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
     1997           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
     1998       | (* short *)
     1999       | (* medium *)
     2000       ] *)
    19872001  |5: (* Call *)
    19882002  |6: (* Mov *)
Note: See TracChangeset for help on using the changeset viewer.