Changeset 2032 for src/ASM/Policy.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/Policy.ma

    r2018 r2032  
    141141        let a ≝ bitvector_of_nat 16 addr in
    142142        let p ≝ bitvector_of_nat 16 pc in
    143         let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 a in
    144         let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 p in
     143        let 〈fst_5_addr, rest_addr〉 ≝ vsplit bool 5 11 a in
     144        let 〈fst_5_pc, rest_pc〉 ≝ vsplit bool 5 11 p in
    145145        eq_bv 5 fst_5_addr fst_5_pc = true
    146146     | long_jump   ⇒ True
     
    359359            + added
    360360    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in
    361   let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (bitvector_of_nat ? addr) in
    362   let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 (bitvector_of_nat ? (\fst inc_sigma)) in
     361  let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (bitvector_of_nat ? addr) in
     362  let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 (bitvector_of_nat ? (\fst inc_sigma)) in
    363363  if eq_bv ? fst_5_addr fst_5_pc
    364364  then medium_jump
     
    655655 [1: #pi cases pi
    656656   [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    657      [1,2,3,6,7,24,25: #x #y
    658      |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    659      #H cases H
    660    |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    661      #_ cases a cases b
    662      [1,5,7,8,9: #_ / by refl/
    663      |10,14,16,17,18: #_ / by refl/
    664      |19,23,25,26,27: #_ / by refl/
    665      |28,32,34,35,36: #_ / by refl/
    666      |37,41,43,44,45: #_ / by refl/
    667      |46,50,52,53,54: #_ / by refl/
    668      |55,59,61,62,63: #_ / by refl/
    669      |64,68,70,71,72: #_ / by refl/
    670      |73,77,79,80,81: #_ / by refl/
    671      |2,3,4,6: cases x #a cases a
    672        [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb
    673        |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb
    674        |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb
    675        |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb
    676        |5,6,7,10,11,12,13,14: #Hb cases Hb
    677        |24,25,26,29,30,31,32,33: #Hb cases Hb
    678        |43,44,45,48,49,50,51,52: #Hb cases Hb
    679        |62,63,64,67,68,69,70,71: #Hb cases Hb
    680        |15,34,53,72: #b #Hb #H normalize in H; destruct (H)
    681        ]
    682      |11,12,13,15: cases x #a cases a
    683        [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb
    684        |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb
    685        |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb
    686        |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb
    687        |5,6,7,10,11,12,13,14: #Hb cases Hb
    688        |24,25,26,29,30,31,32,33: #Hb cases Hb
    689        |43,44,45,48,49,50,51,52: #Hb cases Hb
    690        |62,63,64,67,68,69,70,71: #Hb cases Hb
    691        |15,34,53,72: #b #Hb #H normalize in H; destruct (H)
    692        ]
    693      |20,21,22,24: cases x #a cases a
    694        [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb
    695        |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb
    696        |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb
    697        |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb
    698        |5,6,7,10,11,12,13,14: #Hb cases Hb
    699        |24,25,26,29,30,31,32,33: #Hb cases Hb
    700        |43,44,45,48,49,50,51,52: #Hb cases Hb
    701        |62,63,64,67,68,69,70,71: #Hb cases Hb
    702        |15,34,53,72: #b #Hb #H normalize in H; destruct (H)
    703        ]
    704      |29,30,31,33: cases x #a cases a #a1 #a2
    705        [1,3,5,7: cases a2 #b cases b
    706          [2,3,4,9,15,16,17,18,19: #b #Hb cases Hb
    707          |21,22,23,28,34,35,36,37,38: #b #Hb cases Hb
    708          |40,41,42,47,53,54,55,56,57: #b #Hb cases Hb
    709          |59,60,61,66,72,73,74,75,76: #b #Hb cases Hb
    710          |5,6,7,10,11,12,13,14: #Hb cases Hb
    711          |24,25,26,29,30,31,32,33: #Hb cases Hb
    712          |43,44,45,48,49,50,51,52: #Hb cases Hb
    713          |62,63,64,67,68,69,70,71: #Hb cases Hb
    714          |1,8: #b #Hb #H normalize in H; destruct (H)
    715          |20,27: #b #Hb #H normalize in H; destruct (H)
    716          |39,46: #b #Hb #H normalize in H; destruct (H)
    717          |58,65: #b #Hb #H normalize in H; destruct (H)
    718          ]
    719        |2,4,6,8: cases a1 #b cases b
    720          [1,3,8,9,15,16,17,18,19: #b #Hb cases Hb
    721          |20,22,27,28,34,35,36,37,38: #b #Hb cases Hb
    722          |39,41,46,47,53,54,55,56,57: #b #Hb cases Hb
    723          |58,60,65,66,72,73,74,75,76: #b #Hb cases Hb
    724          |5,6,7,10,11,12,13,14: #Hb cases Hb
    725          |24,25,26,29,30,31,32,33: #Hb cases Hb
    726          |43,44,45,48,49,50,51,52: #Hb cases Hb
    727          |62,63,64,67,68,69,70,71: #Hb cases Hb
    728          |2,4: #b #Hb #H normalize in H; destruct (H)
    729          |21,23: #b #Hb #H normalize in H; destruct (H)
    730          |40,42: #b #Hb #H normalize in H; destruct (H)
    731          |59,61: #b #Hb #H normalize in H; destruct (H)
    732          ]
    733        ]
    734      |38,39,40,42: cases x #a cases a
    735        [2,3,8,9,15,16,17,18,19: #b #Hb cases Hb
    736        |21,22,27,28,34,35,36,37,38: #b #Hb cases Hb
    737        |40,41,46,47,53,54,55,56,57: #b #Hb cases Hb
    738        |59,60,65,66,72,73,74,75,76: #b #Hb cases Hb
    739        |5,6,7,10,11,12,13,14: #Hb cases Hb
    740        |24,25,26,29,30,31,32,33: #Hb cases Hb
    741        |43,44,45,48,49,50,51,52: #Hb cases Hb
    742        |62,63,64,67,68,69,70,71: #Hb cases Hb
    743        |1,4: #b #Hb #H normalize in H; destruct (H)
    744        |20,23: #b #Hb #H normalize in H; destruct (H)
    745        |39,42: #b #Hb #H normalize in H; destruct (H)
    746        |58,61: #b #Hb #H normalize in H; destruct (H)
    747        ]
    748      |47,48,49,51: cases x #a #H normalize in H; destruct (H)
    749      |56,57,58,60: cases x #a #H normalize in H; destruct (H)
    750      |65,66,67,69: cases x #a #H normalize in H; destruct (H)
    751      |74,75,76,78: cases x #a #H normalize in H; destruct (H)
    752      ]
     657     try (#x #y #H #_) try (#x #H #_) try (#H #_) cases H
     658   |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #_ try (#_ %)
     659     try (#abs normalize in abs; destruct (abs) @I)
     660     cases a; cases b; try (#_ %) try (#abs normalize in abs; destruct(abs) @I)
     661     try (@(subaddressing_mode_elim … x) #w #abs normalize in abs; destruct (abs) @I)
     662     cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w
     663     try ( #abs normalize in abs; destruct (abs) @I)
     664     @(subaddressing_mode_elim … a1) #w2 #abs normalize in abs; destruct (abs)
    753665   ]
    754666  |2,3,6: #x [3: #y] #H cases H
Note: See TracChangeset for help on using the changeset viewer.