Changeset 2032 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 8, 2012, 4:32:03 PM (8 years ago)
Author:
sacerdot
Message:

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2028 r2032  
    212212                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
    213213                  [ DATA16 w ⇒ λ_.
    214                      let b1_b2 ≝ split ? 8 8 w in
     214                     let b1_b2 ≝ vsplit ? 8 8 w in
    215215                     let b1 ≝ \fst b1_b2 in
    216216                     let b2 ≝ \snd b1_b2 in
     
    364364     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    365365      [ ADDR11 w ⇒ λ_.
    366          let v1_v2 ≝ split ? 3 8 w in
     366         let v1_v2 ≝ vsplit ? 3 8 w in
    367367         let v1 ≝ \fst v1_v2 in
    368368         let v2 ≝ \snd v1_v2 in
     
    372372     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    373373      [ ADDR11 w ⇒ λ_.
    374          let v1_v2 ≝ split ? 3 8 w in
     374         let v1_v2 ≝ vsplit ? 3 8 w in
    375375         let v1 ≝ \fst v1_v2 in
    376376         let v2 ≝ \snd v1_v2 in
     
    382382     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    383383      [ ADDR16 w ⇒ λ_.
    384          let b1_b2 ≝ split ? 8 8 w in
     384         let b1_b2 ≝ vsplit ? 8 8 w in
    385385         let b1 ≝ \fst b1_b2 in
    386386         let b2 ≝ \snd b1_b2 in
     
    390390     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    391391      [ ADDR16 w ⇒ λ_.
    392          let b1_b2 ≝ split ? 8 8 w in
     392         let b1_b2 ≝ vsplit ? 8 8 w in
    393393         let b1 ≝ \fst b1_b2 in
    394394         let b2 ≝ \snd b1_b2 in
     
    431431   let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    432432   let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_address false in
    433    let 〈upper, lower〉 ≝ split ? 8 8 result in
     433   let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
    434434   if eq_bv ? upper (zero 8) then
    435435     let address ≝ RELATIVE lower in
     
    535535  | Comment comment ⇒ [ ]
    536536  | Call call ⇒
    537     let 〈addr_5, resta〉 ≝ split ? 5 11 (sigma (lookup_labels call)) in
     537    let 〈addr_5, resta〉 ≝ vsplit ? 5 11 (sigma (lookup_labels call)) in
    538538    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    539539    let do_a_long ≝ policy ppc in
    540     let 〈pc_5, restp〉 ≝ split ? 5 11 pc_plus_jmp_length in
     540    let 〈pc_5, restp〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in
    541541    if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then
    542542      let address ≝ ADDR11 resta in
     
    554554    let lookup_address ≝ sigma (lookup_labels jmp) in
    555555    let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_address false in
    556     let 〈upper, lower〉 ≝ split ? 8 8 result in
     556    let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
    557557    if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then
    558558      let address ≝ RELATIVE lower in
    559559        [ SJMP address ]
    560560    else
    561       let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (sigma (lookup_labels jmp)) in
    562       let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc_plus_jmp_length in
     561      let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (sigma (lookup_labels jmp)) in
     562      let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in
    563563      if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then
    564564        let address ≝ ADDR11 rest_addr in
     
    866866
    867867(*CSC: FALSE!!!*)
    868 axiom fetch_pseudo_instruction_split:
     868axiom fetch_pseudo_instruction_vsplit:
    869869 ∀instr_list,ppc.
    870870  ∃pre,suff,lbl.
     
    936936   cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %]
    937937   #res #K
    938    cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
     938   cases (fetch_pseudo_instruction_vsplit (\snd program) ppc) #pre * #suff * #lbl #EQ1
    939939   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?;
    940940   cases daemon (* CSC: XXXXXXXX Ero qui
Note: See TracChangeset for help on using the changeset viewer.