Changeset 1064


Ignore:
Timestamp:
Jul 12, 2011, 5:52:07 PM (8 years ago)
Author:
mulligan
Message:

changes from today, nearly complete rtlabs translation pass

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1063 r1064  
    3333  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
    3434  ].
     35 
     36let rec fold_left2
     37  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → A) (accu: A)
     38  (left: list B) (right: list C) (proof: |left| = |right|)
     39    on left: A ≝
     40  match left return λx. |x| = |right| → A with
     41  [ nil ⇒ λnil_prf.
     42    match right return λx. |[ ]| = |x| → A with
     43    [ nil ⇒ λnil_nil_prf. accu
     44    | cons hd tl ⇒ λcons_nil_absrd. ?
     45    ] nil_prf
     46  | cons hd tl ⇒ λcons_prf.
     47    match right return λx. |hd::tl| = |x| → A with
     48    [ nil ⇒ λcons_nil_absrd. ?
     49    | cons hd' tl' ⇒ λcons_cons_prf.
     50        fold_left2 …  f (f accu hd hd') tl tl' ?
     51    ] cons_prf
     52  ] proof.
     53  [ 1: normalize in cons_nil_absrd;
     54       destruct(cons_nil_absrd)
     55  | 2: normalize in cons_nil_absrd;
     56       destruct(cons_nil_absrd)
     57  | 3: normalize in cons_cons_prf;
     58       @injective_S
     59       assumption
     60  ]
     61qed.
    3562
    3663let rec remove_n_first_internal
     
    96123    foldi_from_until A 0 (|l|) f a l.
    97124
    98 definition hd
     125definition hd_safe
    99126  λA: Type[0].
    100127  λl: list A.
     
    103130  [ nil ⇒ λnil_absrd. ?
    104131  | cons hd tl ⇒ λcons_prf. hd
    105   ].
     132  ] proof.
    106133  normalize in nil_absrd;
    107134  cases(not_le_Sn_O 0)
     
    110137qed.
    111138
    112 definition tail
     139definition tail_safe
    113140  λA: Type[0].
    114141  λl: list A.
     
    117144  [ nil ⇒ λnil_absrd. ?
    118145  | cons hd tl ⇒ λcons_prf. tl
    119   ].
     146  ] proof.
    120147  normalize in nil_absrd;
    121148  cases(not_le_Sn_O 0)
     
    491518  [ nil ⇒ nil A
    492519  | cons hd tl ⇒ (rev A tl) @ [ hd ]
    493   ].
     520  ].
     521
     522lemma append_length:
     523  ∀A: Type[0].
     524  ∀l, r: list A.
     525    |(l @ r)| = |l| + |r|.
     526  #A #L #R
     527  elim L
     528  [ %
     529  | #HD #TL #IH
     530    normalize >IH %
     531  ]
     532qed.
     533
     534lemma append_nil:
     535  ∀A: Type[0].
     536  ∀l: list A.
     537    l @ [ ] = l.
     538  #A #L
     539  elim L //
     540qed.
     541
     542lemma rev_append:
     543  ∀A: Type[0].
     544  ∀l, r: list A.
     545    rev A (l @ r) = rev A r @ rev A l.
     546  #A #L #R
     547  elim L
     548  [ normalize >append_nil %
     549  | #HD #TL #IH
     550    normalize >IH
     551    @associative_append
     552  ]
     553qed.
     554
     555lemma rev_length:
     556  ∀A: Type[0].
     557  ∀l: list A.
     558    |rev A l| = |l|.
     559  #A #L
     560  elim L
     561  [ %
     562  | #HD #TL #IH
     563    normalize
     564    >(append_length A (rev A TL) [HD])
     565    normalize /2/
     566  ]
     567qed.
    494568   
    495569notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
  • src/RTL/RTL.ma

    r1061 r1064  
    1414  | rtl_st_int: register → Byte → label → rtl_statement
    1515  | rtl_st_move: register → register → label → rtl_statement
     16  | rtl_st_clear_carry: label → rtl_statement
    1617  | rtl_st_opaccs: OpAccs → register → register → register → register → label → rtl_statement
    1718  | rtl_st_op1: Op1 → register → register → label → rtl_statement
    1819  | rtl_st_op2: Op2 → register → register → register → label → rtl_statement
    19   | rtl_st_clear_carry: label → rtl_statement
    2020  | rtl_st_load: register → register → register → label → rtl_statement
    2121  | rtl_st_store: register → register → register → label → rtl_statement
     
    2626  | rtl_st_cond_acc: register → label → label → rtl_statement
    2727  | rtl_st_set_carry: label → rtl_statement
    28   | rtl_st_clear_carry: label → rtl_statement
    2928  | rtl_st_return: registers → rtl_statement.
    3029 
  • src/RTLabs/RTLAbstoRTL.ma

    r1063 r1064  
    125125      〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
    126126
     127(* obvious, but proof doesn't look easy! *)
     128axiom complete_regs_length:
     129  ∀def.
     130  ∀left.
     131  ∀right.
     132    |\fst (\fst (complete_regs def left right))| = |\snd (\fst (complete_regs def left right))|.
     133
    127134definition size_of_sig_type ≝
    128135  λsig.
     
    240247  | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
    241248  | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
    242   | rtl_st_clear_carry _ ⇒ rtl_st_clear_carry lbl
    243249  | rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl
    244250  | rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl
     
    460466  ].
    461467
    462 definition translate_intermediate_op1 ≝
    463   λop1.
    464   λdestrs.
    465   λsrcrs.
    466   λstart_lbl.
    467   λdest_lbl.
    468   λdef.
     468definition translate_op1 ≝
     469  λop1: op1.
     470  λdestrs: list register.
     471  λsrcrs: list register.
    469472  λprf: |destrs| = |srcrs|.
     473  λstart_lbl: label.
     474  λdest_lbl: label.
     475  λdef: rtl_internal_function.
    470476  match op1 with
    471   [ intermediate_op1_cast src_size src_sign dest_size ⇒
     477  [ op_cast src_size src_sign dest_size ⇒
    472478      translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
    473   | intermediate_op1_negint ⇒
     479  | op_neg_int ⇒
    474480      translate_negint destrs srcrs start_lbl dest_lbl def prf
    475   | intermediate_op1_notbool ⇒
     481  | op_not_bool ⇒
    476482      translate_notbool destrs srcrs start_lbl dest_lbl def
    477   | intermediate_op1_notint ⇒
     483  | op_not_int ⇒
    478484    let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
    479485    let l ≝ map2 … f destrs srcrs prf in
    480486      adds_graph l start_lbl dest_lbl def
    481   | intermediate_op1_ptrofint ⇒
     487  | op_ptr_of_int ⇒
    482488      translate_move destrs srcrs start_lbl dest_lbl def
    483   | intermediate_op1_intofptr ⇒
     489  | op_int_of_ptr ⇒
    484490      translate_move destrs srcrs start_lbl dest_lbl def
    485   | intermediate_op1_id ⇒
     491  | op_id ⇒
    486492      translate_move destrs srcrs start_lbl dest_lbl def
    487493  ].
     
    618624    translates @ tmp_destrs2'.
    619625
     626axiom translate_mul:
     627  ∀destrs: list register.
     628  ∀srcrs1: list register.
     629  ∀srcrs2: list register.
     630  ∀start_lbl: label.
     631  ∀dest_lbl: label.
     632  ∀def: rtl_internal_function.
     633    rtl_internal_function.
     634
     635(*
    620636definition translate_mul ≝
    621637  λdestrs: list register.
     
    639655  let insts_mul ≝ foldi ? ? [ ] srcrs2 in ?. [5: check insts_init.
    640656    add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
    641 
    642 let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
    643   let (def, dummy) = fresh_reg def in
    644   let (def, tmpr) = fresh_reg def in
    645   let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
    646   let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in
    647   let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in
    648   let insts_init =
    649     [translate_move fresh_srcrs1 srcrs1 ;
    650      translate_move fresh_srcrs2 srcrs2 ;
    651      translate_cst (AST.Cst_int 0) destrs] in
    652   let f = λi. translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl i ? in
    653   let insts_mul = MiscPottier.foldi f [] srcrs2 in
    654   add_translates (insts_init @ insts_mul) start_lbl dest_lbl def
     657*)
     658
     659definition translate_divumodu8 ≝
     660  λorder: bool.
     661  λdestrs: list register.
     662  λsrcr1: register.
     663  λsrcr2: register.
     664  λstart_lbl: label.
     665  λdest_lbl: label.
     666  λdef: rtl_internal_function.
     667  match destrs with
     668  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     669  | cons destr destrs ⇒
     670    let 〈def, dummy〉 ≝ fresh_reg def in
     671    let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉 | _ ⇒ 〈dummy, destr〉 ] in
     672    let inst_div ≝ adds_graph [
     673      rtl_st_opaccs DivuModu destr1 destr2 srcr1 srcr2 start_lbl
     674    ]
     675    in
     676    let insts_rest ≝ translate_cst (Ointconst I8 (zero ?)) destrs in
     677      add_translates [ inst_div; insts_rest ] start_lbl dest_lbl def
     678  ].
     679
     680definition translate_ne: ? → ? → ? → ? → ? → ? → rtl_internal_function ≝
     681  λdestrs: list register.
     682  λsrcrs1: list register.
     683  λsrcrs2: list register.
     684  λstart_lbl: label.
     685  λdest_lbl: label.
     686  λdef: rtl_internal_function.
     687  match destrs with
     688  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     689  | cons destr destrs ⇒
     690    let 〈def, tmpr〉 ≝ fresh_reg def in
     691    let 〈def, tmp_zero〉 ≝ fresh_reg def in
     692    let 〈def, tmp_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
     693    let save_srcrs1 ≝ translate_move tmp_srcrs1 srcrs1 in
     694    let 〈def, tmp_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
     695    let save_srcrs2 ≝ translate_move tmp_srcrs2 srcrs2 in
     696    match reduce_strong ? tmp_srcrs1 tmp_srcrs2 with
     697    [ dp crl their_proof ⇒
     698      let commonl ≝ \fst (\fst crl) in
     699      let commonr ≝ \fst (\snd crl) in
     700      let restl ≝ \snd (\snd crl) in
     701      let restr ≝ \snd (\snd crl) in
     702      let rest ≝ choose_rest ? restl restr ? ? in
     703      let inits ≝ [
     704        rtl_st_int destr (zero ?) start_lbl;
     705        rtl_st_int tmp_zero (zero ?) start_lbl
     706      ]
     707      in
     708      let f_common ≝ λtmp_srcr1. λtmp_srcr2. [
     709        rtl_st_clear_carry start_lbl;
     710        rtl_st_op2 Sub tmpr tmp_srcr1 tmp_srcr2 start_lbl;
     711        rtl_st_op2 Or destr destr tmpr start_lbl
     712      ]
     713      in
     714      let insts_common ≝ flatten ? (map2 … f_common commonl commonr ?) in
     715      let f_rest ≝ λtmp_srcr. [
     716        rtl_st_clear_carry start_lbl;
     717        rtl_st_op2 Sub tmpr tmp_zero tmp_srcr start_lbl;
     718        rtl_st_op2 Or destr destr tmpr start_lbl
     719      ]
     720      in
     721      let insts_rest ≝ flatten ? (map ? ? f_rest rest) in
     722      let insts ≝ inits @ insts_common @ insts_rest in
     723      let epilogue ≝ translate_cst (Ointconst I8 (zero ?)) destrs in
     724        add_translates [
     725          save_srcrs1; save_srcrs2; adds_graph insts; epilogue
     726        ] start_lbl dest_lbl def
     727    ]
     728  ].
     729  [1: @their_proof
     730  |*: cases not_implemented (* choose rest requires non-emptiness proofs but
     731                               these appear impossible to obtain, similar proof
     732                               to above *)
     733  ]
     734qed.
     735
     736definition translate_eq_reg ≝
     737  λtmp_zero: register.
     738  λtmp_one: register.
     739  λtmpr1: register.
     740  λtmpr2: register.
     741  λdestr: register.
     742  λdummy_lbl: label.
     743  λsrcr12: register × register.
     744  let 〈srcr1, srcr2〉 ≝ srcr12 in
     745  [ rtl_st_clear_carry dummy_lbl;
     746    rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;
     747    rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;
     748    rtl_st_op2 Sub tmpr2 srcr2 srcr1 dummy_lbl;
     749    rtl_st_op2 Addc tmpr2 tmp_zero tmp_zero dummy_lbl;
     750    rtl_st_op2 Or tmpr1 tmpr1 tmpr2 dummy_lbl;
     751    rtl_st_op2 Xor tmpr1 tmpr1 tmp_one dummy_lbl;
     752    rtl_st_op2 And destr destr tmpr1 dummy_lbl ].
     753
     754definition translate_eq_list ≝
     755  λtmp_zero: register.
     756  λtmp_one: register.
     757  λtmpr1: register.
     758  λtmpr2: register.
     759  λdestr: register.
     760  λleq: list (register × register).
     761  λdummy_lbl: label.
     762  let f ≝ translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
     763    (rtl_st_int destr (bitvector_of_nat ? 1) dummy_lbl) ::
     764      flatten ? (map ? ? f leq).
     765
     766definition translate_atom ≝
     767  λtmp_zero: register.
     768  λtmp_one: register.
     769  λtmpr1: register.
     770  λtmpr2: register.
     771  λtmpr3: register.
     772  λdestr: register.
     773  λdummy_lbl: label.
     774  λleq: list (register × register).
     775  λsrcr1: register.
     776  λsrcr2: register.
     777    translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @
     778    [ rtl_st_clear_carry dummy_lbl;
     779      rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;
     780      rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;
     781      rtl_st_op2 And tmpr3 tmpr3 tmpr1 dummy_lbl;
     782      rtl_st_op2 Or destr destr tmpr3 dummy_lbl ].
     783
     784definition translate_lt_main ≝
     785  λtmp_zero: register.
     786  λtmp_one: register.
     787  λtmpr1: register.
     788  λtmpr2: register.
     789  λtmpr3: register.
     790  λdestr: register.
     791  λdummy_lbl: label.
     792  λsrcrs1: list register.
     793  λsrcrs2: list register.
     794  λproof: |srcrs1| = |srcrs2|.
     795  let f ≝ λinsts_leq. λsrcr1. λsrcr2.
     796    let 〈insts, leq〉 ≝ insts_leq in
     797    let added_insts ≝ translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in
     798      〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉
     799  in
     800    \fst (fold_left2 ? ? ? f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).
     801
     802definition fresh_regs_strong:
     803  rtl_internal_function → ∀n: nat. Σfresh: rtl_internal_function × (list register). |\snd fresh| = n ≝
     804  λdef.
     805  λn.
     806    fresh_regs def n.
     807  @fresh_regs_length
     808qed.
     809
     810definition complete_regs_strong:
     811  rtl_internal_function → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝
     812  λdef.
     813  λleft.
     814  λright.
     815    complete_regs def left right.
     816  @complete_regs_length
     817qed.
     818
     819definition translate_lt ≝
     820  λdestrs: list register.
     821  λprf_destrs: lt 0 (|destrs|).
     822  λsrcrs1: list register.
     823  λsrcrs2: list register.
     824  λprf_srcrs: |srcrs1| = |srcrs2|.
     825  λstart_lbl: label.
     826  λdest_lbl: label.
     827  λdef: rtl_internal_function.
     828  match destrs with
     829  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     830  | _ ⇒
     831    match fresh_regs_strong def (|destrs|) with
     832    [ dp def_tmp_destrs tmp_destrs_proof ⇒
     833      let def ≝ \fst def_tmp_destrs in
     834      let tmp_destrs ≝ \snd def_tmp_destrs in
     835      let tmp_destr ≝ hd_safe ? tmp_destrs ? in
     836      let 〈def, tmp_zero〉 ≝ fresh_reg def in
     837      let 〈def, tmp_one〉 ≝ fresh_reg def in
     838      let 〈def, tmpr1〉 ≝ fresh_reg def in
     839      let 〈def, tmpr2〉 ≝ fresh_reg def in
     840      let 〈def, tmpr3〉 ≝ fresh_reg def in
     841      match complete_regs_strong def srcrs1 srcrs2 with
     842      [ dp srcrs12_added srcrs12_proof ⇒
     843        let srcrs1 ≝ \fst (\fst srcrs12_added) in
     844        let srcrs2 ≝ \snd (\fst srcrs12_added) in
     845        let added ≝ \snd srcrs12_added in
     846        let srcrs1' ≝ rev ? srcrs1 in
     847        let srcrs2' ≝ rev ? srcrs2 in
     848        let insts_init ≝ [
     849          translate_cst (Ointconst I8 (zero ?)) tmp_destrs;
     850          translate_cst (Ointconst I8 (zero ?)) added;
     851          adds_graph [
     852            rtl_st_int tmp_zero (zero ?) start_lbl;
     853            rtl_st_int tmp_one (bitvector_of_nat ? 1) start_lbl
     854          ]
     855        ]
     856        in
     857        let insts_main ≝
     858          translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in
     859          let insts_main ≝ [ adds_graph insts_main ] in
     860          let insts_exit ≝ [ translate_move destrs tmp_destrs ] in
     861            add_translates (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def
     862      ]
     863    ]
     864  ].
     865  [2: >tmp_destrs_proof @prf_destrs
     866  |1: normalize nodelta
     867      generalize in match srcrs12_proof
     868      #HYP >rev_length >rev_length @HYP
     869  ]
     870qed.
     871
     872definition add_128_to_last ≝
     873  λtmp_128: register.
     874  λrs.
     875  λprf: 0 < |rs|.
     876  λstart_lbl: label.
     877  match rs with
     878  [ nil ⇒ adds_graph [ ] start_lbl
     879  | _ ⇒
     880    let r ≝ last_safe ? rs prf in
     881      adds_graph [
     882        rtl_st_op2 Add r r tmp_128 start_lbl
     883      ] start_lbl
     884  ].
     885
     886definition translate_lts ≝
     887  λdestrs: list register.
     888  λdestrs_prf: lt 0 (|destrs|).
     889  λsrcrs1: list register.
     890  λsrcrs2: list register.
     891  λsrcrs_prf: |srcrs1| = |srcrs2|.
     892  λsrcrs1_lt_prf: 0 < |srcrs1|.
     893  λstart_lbl: label.
     894  λdest_lbl: label.
     895  λdef: rtl_internal_function.
     896  match fresh_regs_strong def (|srcrs1|) with
     897  [ dp def_tmp_srcrs1 srcrs1_prf ⇒
     898    let def ≝ \fst def_tmp_srcrs1 in
     899    let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in
     900    match fresh_regs_strong def (|srcrs2|) with
     901    [ dp def_tmp_srcrs2 srcrs2_prf ⇒
     902      let def ≝ \fst def_tmp_srcrs2 in
     903      let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in
     904      let 〈def, tmp_128〉 ≝ fresh_reg def in
     905        add_translates [
     906          translate_move tmp_srcrs1 srcrs1;
     907          translate_move tmp_srcrs2 srcrs2;
     908          adds_graph [
     909            rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl
     910          ];
     911          add_128_to_last tmp_128 tmp_srcrs1 ?;
     912          add_128_to_last tmp_128 tmp_srcrs2 ?;
     913          translate_lt destrs destrs_prf tmp_srcrs1 tmp_srcrs2 ?
     914        ] start_lbl dest_lbl def
     915    ]
     916  ].
     917  [2: >srcrs2_prf >srcrs1_prf @srcrs_prf
     918  |3: >srcrs2_prf <srcrs_prf @srcrs1_lt_prf
     919  |1: >srcrs1_prf @srcrs1_lt_prf
     920  ]
     921qed.
     922
     923definition translate_op2 ≝
     924  λop2.
     925  λdestrs: list register.
     926  λdestrs_prf: lt 0 (|destrs|).
     927  λsrcrs1: list register.
     928  λsrcrs2: list register.
     929  λsrcrs_prf: |srcrs1| = |srcrs2|.
     930  λstart_lbl: label.
     931  λdest_lbl: label.
     932  λdef: rtl_internal_function.
     933  match op2 with
     934  [ op_add ⇒
     935    translate_op Addc destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
     936  | op_addp ⇒
     937    translate_op Addc destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
     938  | op_sub ⇒
     939    translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
     940  | op_subp ⇒
     941    translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
     942  | op_subpp ⇒
     943    translate_op Sub destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
     944  | op_mul ⇒
     945    translate_op Mul destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
     946  | op_divu ⇒ ?
     947  | op_modu ⇒ ?
     948  | op_and ⇒
     949    translate_op And destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
     950  | op_or ⇒
     951    translate_op Or destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
     952  | op_xor ⇒
     953    translate_op Xor destrs srcrs1 srcrs2 srcrs_prf start_lbl dest_lbl def
     954  | op_cmp c ⇒
     955    match c with
     956    [ Compare_Equal ⇒
     957      add_translates [
     958        translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def;
     959        translate_op1 op_not_bool destrs destrs (refl ? (|destrs|))
     960      ] start_lbl dest_lbl def
     961    | Compare_NotEqual ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
     962    | Compare_Less ⇒ translate_lts destrs destrs_prf srcrs1 srcrs2 srcrs_prf ? start_lbl dest_lbl def
     963    | Compare_Greater ⇒ translate_lts destrs destrs_prf srcrs2 srcrs1 srcrs_prf ? start_lbl dest_lbl def
     964    | Compare_LessEqual ⇒
     965      add_translates [
     966        translate_lts destrs destrs_prf srcrs2 srcrs1 srcrs_prf ? start_lbl dest_lbl def;
     967        translate_op1 op_not_bool destrs destrs (refl ? (|destrs|))
     968      ] start_lbl dest_lbl def
     969    | Compare_GreaterEqual ⇒
     970      add_translates [
     971        translate_lts destrs destrs_prf srcrs1 srcrs2 srcrs_prf ? start_lbl dest_lbl def;
     972        translate_op1 op_not_bool destrs destrs (refl ? (|destrs|))
     973      ] start_lbl dest_lbl def
     974    ]
     975  | _ ⇒ ?
     976  ].
     977
     978let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
     979  match op2 with
     980
     981    | AST.Op_divu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
     982      translate_divumodu8 true destrs (List.hd srcrs1) (List.hd srcrs2)
     983        start_lbl dest_lbl def
     984
     985    | AST.Op_modu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
     986      translate_divumodu8 false destrs (List.hd srcrs1) (List.hd srcrs2)
     987        start_lbl dest_lbl def
     988
     989    | AST.Op_cmp AST.Cmp_eq
     990    | AST.Op_cmpu AST.Cmp_eq
     991    | AST.Op_cmpp AST.Cmp_eq ->
     992      add_translates
     993        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) destrs srcrs1 srcrs2 ;
     994         translate_op1 AST.Op_notbool destrs destrs]
     995        start_lbl dest_lbl def
     996
     997    | AST.Op_cmp AST.Cmp_ne
     998    | AST.Op_cmpu AST.Cmp_ne
     999    | AST.Op_cmpp AST.Cmp_ne ->
     1000      translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
     1001
     1002    | AST.Op_cmp AST.Cmp_lt ->
     1003      translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def
     1004
     1005    | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt ->
     1006      translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def
     1007
     1008    | AST.Op_cmp AST.Cmp_le ->
     1009      add_translates
     1010        [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
     1011         translate_op1 AST.Op_notbool destrs destrs]
     1012        start_lbl dest_lbl def
     1013
     1014    | AST.Op_cmpu AST.Cmp_le ->
     1015      add_translates
     1016        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs2 srcrs1 ;
     1017         translate_op1 AST.Op_notbool destrs destrs]
     1018        start_lbl dest_lbl def
     1019
     1020    | AST.Op_cmpp AST.Cmp_le ->
     1021      add_translates
     1022        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
     1023         translate_op1 AST.Op_notbool destrs destrs]
     1024        start_lbl dest_lbl def
     1025
     1026    | AST.Op_cmp AST.Cmp_gt ->
     1027      translate_op2 (AST.Op_cmp AST.Cmp_lt)
     1028        destrs srcrs2 srcrs1 start_lbl dest_lbl def
     1029
     1030    | AST.Op_cmpu AST.Cmp_gt ->
     1031      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
     1032        destrs srcrs2 srcrs1 start_lbl dest_lbl def
     1033
     1034    | AST.Op_cmpp AST.Cmp_gt ->
     1035      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
     1036        destrs srcrs2 srcrs1 start_lbl dest_lbl def
     1037
     1038    | AST.Op_cmp AST.Cmp_ge ->
     1039      add_translates
     1040        [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
     1041         translate_op1 AST.Op_notbool destrs destrs]
     1042        start_lbl dest_lbl def
     1043
     1044    | AST.Op_cmpu AST.Cmp_ge ->
     1045      add_translates
     1046        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
     1047         translate_op1 AST.Op_notbool destrs destrs]
     1048        start_lbl dest_lbl def
     1049
     1050    | AST.Op_cmpp AST.Cmp_ge ->
     1051      add_translates
     1052        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
     1053         translate_op1 AST.Op_notbool destrs destrs]
     1054        start_lbl dest_lbl def
     1055
     1056    | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl
     1057    | AST.Op_shr | AST.Op_shru ->
     1058      (* Unsupported, should have been replaced by a runtime function. *)
     1059      assert false
     1060
    6551061
    6561062definition filter_and_to_list_local_env_internal ≝
     
    8631269      rtl_st_cond_acc tmpr lbl_true lbl_false
    8641270    ] start_lbl start_lbl def.
     1271   
     1272   
    8651273
    8661274(*
  • src/common/AST.ma

    r1060 r1064  
    104104  | I32: intsize.
    105105
    106 (* unary operations used in the backend intermediate languages, there's also a separate
    107    type for unary operations at the assembly level in ASM/I8051.ma *)
    108 inductive intermediate_op1: Type[0] ≝
    109   | intermediate_op1_cast: nat → signedness → nat → intermediate_op1 (**r size in bytes, signedness, to size *)
    110   | intermediate_op1_negint: intermediate_op1           (**r integer opposite *)
    111   | intermediate_op1_notbool: intermediate_op1          (**r boolean negation  *)
    112   | intermediate_op1_notint: intermediate_op1           (**r bitwise complement  *)
    113   | intermediate_op1_id: intermediate_op1               (**r identity *)
    114   | intermediate_op1_ptrofint: intermediate_op1         (**r int to pointer *)
    115   | intermediate_op1_intofptr: intermediate_op1.        (**r pointer to int *)
    116 
    117106(* * Float types come in two sizes: 32 bits (single precision)
    118107  and 64-bit (double precision). *)
     
    409398
    410399Remark map_partial_identity:
    411   forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
     400  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),cmp
    412401  map_partial prefix (fun b => OK b) l = OK l.
    413402Proof.
     
    665654
    666655inductive op1: Type[0] ≝
    667   | op_cast8_unsigned: op1   (**r 8-bit zero extension  *)
    668   | op_cast8_signed: op1     (**r 8-bit sign extension  *)
    669   | op_cast16_unsigned: op1  (**r 16-bit zero extension  *)
    670   | op_cast16_signed: op1    (**r 16-bit sign extension *)
     656  | op_cast: nat → signedness → nat → op1
    671657  | op_neg_int: op1          (**r integer opposite *)
    672658  | op_not_bool: op1         (**r boolean negation  *)
    673659  | op_not_int: op1          (**r bitwise complement  *)
    674   | op_negf: op1             (**r float opposite *)
    675   | op_absf: op1             (**r float absolute value *)
    676   | op_single_of_float: op1  (**r float truncation *)
    677   | op_int_of_float: op1     (**r signed integer to float *)
    678   | op_intu_of_float: op1    (**r unsigned integer to float *)
    679   | op_float_of_int: op1     (**r float to signed integer *)
    680   | op_float_of_intu: op1    (**r float to unsigned integer *)
    681660  | op_id: op1               (**r identity *)
    682661  | op_ptr_of_int: op1       (**r int to pointer *)
     
    697676  | op_shr: op2         (**r right signed shift *)
    698677  | op_shru: op2        (**r right unsigned shift *)
    699   | op_addf: op2        (**r float addition *)
    700   | op_subf: op2        (**r float subtraction *)
    701   | op_mulf: op2        (**r float multiplication *)
    702   | op_divf: op2        (**r float division *)
    703678  | op_cmp: Compare → op2   (**r integer signed comparison *)
    704679  | op_cmpu: Compare → op2  (**r integer unsigned comparison *)
    705   | op_cmpf: Compare → op2  (**r float comparison *)
    706680  | op_addp: op2        (**r addition for a pointer and an integer *)
    707681  | op_subp: op2        (**r substraction for a pointer and a integer *)
     682  | op_subpp: op2
    708683  | op_cmpp: Compare → op2. (**r pointer comparaison *)
Note: See TracChangeset for help on using the changeset viewer.