Changeset 2720


Ignore:
Timestamp:
Feb 23, 2013, 12:03:13 PM (6 years ago)
Author:
tranquil
Message:

implemented back end ops that were still axioms

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/BackEndOps.ma

    r2645 r2720  
    11include "common/ByteValues.ma".
     2include "ASM/Arithmetic.ma".
     3
     4(* just to avoid computing div and mod separately *)
     5definition divmodZ ≝ λx,y.
     6  match x with
     7  [ OZ ⇒ 〈OZ, OZ〉
     8  | pos n ⇒
     9    match y with
     10    [ OZ ⇒ 〈OZ, OZ〉
     11    | pos m ⇒ let 〈q, r〉 ≝ divide n m in
     12              〈natp_to_Z q, natp_to_Z r〉
     13    | neg m ⇒ let 〈q, r〉 ≝ divide n m in
     14              match r with
     15              [ pzero ⇒ 〈natp_to_negZ q, OZ〉
     16              | _ ⇒ 〈Zpred (natp_to_negZ q), y+ natp_to_Z r〉
     17              ]
     18    ]
     19  | neg n ⇒
     20    match y with
     21    [ OZ ⇒ 〈OZ, OZ〉
     22    | pos m ⇒ let 〈q,r〉 ≝ divide n m in
     23              match r with
     24              [ pzero ⇒ 〈natp_to_negZ q, OZ〉
     25              | _ ⇒ 〈Zpred (natp_to_negZ q), y- natp_to_Z r〉
     26              ]
     27    | neg m ⇒ let 〈q, r〉 ≝ divide n m in
     28              〈natp_to_Z q, natp_to_Z r〉
     29    ]
     30  ].
    231
    332(* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps
     
    1039  Cmpl: Op1
    1140| Inc: Op1
    12 | Rl: Op1. (* TODO: implement left rotation *)
     41| Rl: Op1.
    1342
    1443inductive Op2: Type[0] ≝
     
    2756}.
    2857
    29 axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte.
    30 axiom op1_implementation: Op1 → Byte → Byte.
    31 axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit).
     58definition opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte ≝
     59λop,by1,by2.
     60(* Paolo: in ASM/Interpret.ma we use nats, but using Z is more efficient, isn't it? *)
     61let n1 ≝ Z_of_unsigned_bitvector … by1 in
     62let n2 ≝ Z_of_unsigned_bitvector … by2 in
     63match op with
     64[ Mul ⇒
     65  let prod ≝ vsplit … (bitvector_of_Z (8 + 8) (n1 * n2)) in
     66  〈\snd prod, \fst prod〉
     67| DivuModu ⇒
     68  if eqZb n2 OZ then
     69    (* to mimic ASM/Interpret.ma, we return the arguments *)
     70    〈by1, by2〉
     71  else
     72    let 〈q, r〉 ≝ divmodZ n1 n2 in
     73    〈bitvector_of_Z … q, bitvector_of_Z … r〉
     74].
     75
     76definition op1_implementation: Op1 → Byte → Byte ≝
     77λop,by.
     78match op with
     79[ Cmpl ⇒
     80  negation_bv ? by
     81| Inc ⇒
     82  add … by (bitvector_of_nat 8 1)
     83| Rl ⇒
     84  rotate_left … 1 by
     85].
     86
     87definition op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit) ≝
     88λcarry,op,by1,by2.
     89match op with
     90[ Add ⇒
     91  let 〈res, flags〉 ≝ add_8_with_carry by1 by2 false in
     92  〈res, get_index' ? O  ? flags〉
     93| Addc ⇒
     94  let 〈res, flags〉 ≝ add_8_with_carry by1 by2 carry in
     95  〈res, get_index' ? O  ? flags〉
     96| Sub ⇒
     97  let 〈res, flags〉 ≝ sub_8_with_carry by1 by2 carry in
     98  〈res, get_index' ? O  ? flags〉
     99| And ⇒
     100  〈conjunction_bv ? by1 by2, carry〉
     101| Or ⇒
     102  〈inclusive_disjunction_bv ? by1 by2, carry〉
     103| Xor ⇒
     104  〈exclusive_disjunction_bv ? by1 by2, carry〉
     105].
    32106
    33107definition eval : Eval ≝
Note: See TracChangeset for help on using the changeset viewer.