source: src/common/BackEndOps.ma @ 2317

Last change on this file since 2317 was 2286, checked in by tranquil, 8 years ago

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell
File size: 7.1 KB
Line 
1include "common/ByteValues.ma".
2
3(* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps
4        not further back in the translation chain.                            *)
5inductive OpAccs: Type[0] ≝
6  Mul: OpAccs
7| DivuModu: OpAccs.
8
9inductive Op1: Type[0] ≝
10  Cmpl: Op1
11| Inc: Op1
12| Rl: Op1. (* TODO: implement left rotation *)
13
14inductive Op2: Type[0] ≝
15  Add: Op2
16| Addc: Op2
17| Sub: Op2
18| And: Op2
19| Or: Op2
20| Xor: Op2.
21
22record Eval : Type[0] ≝
23{
24  opaccs: OpAccs → Byte → Byte → Byte × Byte;
25  op1: Op1 → Byte → Byte;
26  op2: Bit → Op2 → Byte → Byte → (Byte × Bit)
27}.
28
29axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte.
30axiom op1_implementation: Op1 → Byte → Byte.
31axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit).
32
33definition eval : Eval ≝
34  mk_Eval opaccs_implementation
35          op1_implementation
36          op2_implementation.
37
38axiom UnsupportedOp : String.
39
40definition be_opaccs : OpAccs → beval → beval → res (beval × beval) ≝
41  λop,a,b.
42  ! a' ← Byte_of_val UnsupportedOp a ;
43  ! b' ← Byte_of_val UnsupportedOp b ;
44  let 〈a'',b''〉 ≝ opaccs eval op a' b' in
45  return 〈BVByte a'', BVByte b''〉.
46
47definition be_op1 : Op1 → beval → res beval ≝
48  λop,a.
49  ! a' ← Byte_of_val UnsupportedOp a ;
50  return BVByte (op1 eval op a').
51
52definition op2_bytes : Op2 → ∀n.Bit → Vector Byte n → Vector Byte n → (Vector Byte n) × Bit ≝
53λop,n,carry.
54  let f ≝ λn,b1,b2.λpr : (Vector Byte n) × Bit.
55    let 〈res_tl, carry〉 ≝ pr in
56    let 〈res_hd,carry'〉 ≝ op2 eval carry op b1 b2 in
57    〈res_hd ::: res_tl, carry'〉 in
58  fold_right2_i … f 〈[[ ]],carry〉 n.
59
60definition be_add_sub_byte : bool → bebit → beval → Byte → res (beval × bebit) ≝
61  λis_add,carry,a1,b2.
62  let op ≝ if is_add then Addc else Sub in
63  match a1 with
64  [ BVByte b1 ⇒
65    ! carry' ← Bit_of_val UnsupportedOp carry ;
66    let 〈rslt, carry''〉 ≝ op2 eval carry' op b1 b2 in
67    return 〈BVByte rslt, BBbit carry''〉
68  | BVptr b p o ⇒
69    match p with
70    [ O ⇒ λ_:0<size_pointer.λo : Vector Byte 1.
71      if eq_bebit carry (BBbit false) then
72        let o' ≝ from_singl … o in
73        let 〈rslt,carry〉 ≝ op2 eval false op b2 o' in
74        let p' : part ≝ mk_part 0 ? in
75        return 〈BVptr b p' [[rslt]], BBptrcarry is_add b p' o [[b2]]〉
76      else
77        Error … [MSG UnsupportedOp]
78    | S k ⇒ λSk_ok:S k<size_pointer.λo : Vector Byte (S (S k)).
79      match carry with
80      [ BBptrcarry is_add' b' p' o' by' ⇒
81        if eq_b is_add is_add' ∧ eq_block b b' ∧ vsuffix … (eq_bv 8) o' o then
82          If eqb k p' then with prf do
83            let by' ≝ by' ⌈Vector ?? ↦ Vector Byte (S k)⌉ in
84            let 〈rslt,ignore〉 ≝ op2_bytes op … false o (b2 ::: by') in
85            let Sk_part ≝ mk_part (S k) Sk_ok in
86            OK … 〈BVptr b Sk_part rslt,
87                     BBptrcarry is_add b Sk_part o (b2 ::: by')〉
88          else Error … [MSG UnsupportedOp]
89        else Error … [MSG UnsupportedOp]
90      | _ ⇒ Error … [MSG UnsupportedOp]
91      ]
92    ] (part_no_ok p) o
93  | _ ⇒ Error … [MSG UnsupportedOp]
94  ].
95@hide_prf [//]
96lapply prf @(eqb_elim k) #H * >H %
97qed.
98
99(* This tables shows what binary ops may be defined on bevals depending on
100   the arguments (columns marked by 1st argument, rows by 2nd). Further
101   checks for definedness are done for pointer parts taking into account
102   blocks, parts and the carry value.
103            | BVByte    | BVptr          | BVnull | BVnonzero | BVundef |
104  ----------+-----------+----------------+--------+-----------+---------|
105  BVByte    | all       | Add, Addc, Sub | none   | Or        | none    |
106  ----------+-----------+----------------+--------+-----------+---------|
107  BVptr     | Add, Addc | Sub, Xor       | Xor    | none      | none    |
108  ----------+-----------+----------------+--------+-----------+---------|
109  BVnull    | none      | Xor            | Xor    | none      | none    |
110  ----------+-----------+----------------+--------+-----------+---------|
111  BVnonzero | Or        | none           | none   | Or        | none    |
112  ----------+-----------+----------------+--------+-----------+---------|
113  BVundef   | none      | none           | none   | none      | none    |
114  ----------------------------------------------------------------------+
115*)
116definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝
117  λcarry,op,a1,a2.
118  match a1 with
119  [ BVByte b1 ⇒
120    match a2 with
121    [ BVByte b2 ⇒
122      ! carry ← Bit_of_val UnsupportedOp carry ;
123      let 〈result, carry〉 ≝ op2 eval carry op b1 b2 in
124      return 〈BVByte result, BBbit carry〉
125    | BVptr bl2 p2 o2 ⇒
126      match op with
127      [ Add ⇒ be_add_sub_byte true (BBbit false) a2 b1
128      | Addc ⇒ be_add_sub_byte true carry a2 b1
129      | _ ⇒ Error … [MSG UnsupportedOp]
130      ]
131    | BVnonzero ⇒
132      match op with
133      [ Or ⇒ return 〈BVnonzero, carry〉
134      | _ ⇒ Error … [MSG UnsupportedOp]
135      ]
136    | _ ⇒ Error … [MSG UnsupportedOp]
137    ]
138  | BVptr bl1 p1 o1 ⇒
139    match a2 with
140    [ BVByte b2 ⇒
141      match op with
142      [ Add ⇒ be_add_sub_byte true (BBbit false) a1 b2
143      | Addc ⇒ be_add_sub_byte true carry a1 b2
144      | Sub ⇒ be_add_sub_byte false carry a1 b2
145      | _ ⇒ Error … [MSG UnsupportedOp]
146      ]
147    | BVptr bl2 p2 o2 ⇒
148      match op with
149      [ Sub ⇒
150        if eq_block bl1 bl2 ∧ eqb p1 p2 then
151          ! carry ← Bit_of_val UnsupportedOp carry ;
152          let by1 ≝ head' … o1 in
153          let by2 ≝ head' … o2 in
154          let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in
155          return 〈BVByte result, BBbit carry〉
156        else Error … [MSG UnsupportedOp]
157      | Xor ⇒
158        if eq_block bl1 bl2 ∧ eqb p1 p2 then
159          if vprefix … (eq_bv 8) o1 o2 (* equivalent to equality *) then
160            return 〈BVByte (bv_zero …), carry〉
161          else
162            return 〈BVnonzero, carry〉
163        else Error … [MSG UnsupportedOp]
164      | _ ⇒ Error … [MSG UnsupportedOp]
165      ]
166    | BVnull p2 ⇒
167      match op with
168      [ Xor ⇒
169        if eqb p1 p2 then
170          return 〈BVnonzero, carry〉
171        else
172          Error … [MSG UnsupportedOp]
173      | _ ⇒ Error … [MSG UnsupportedOp]
174      ]
175    | _ ⇒ Error … [MSG UnsupportedOp]
176    ]
177  | BVnonzero ⇒
178    match op with
179    [ Or ⇒
180      match a2 with
181      [ BVByte _ ⇒ return 〈BVnonzero, carry〉
182      | BVnonzero ⇒ return 〈BVnonzero, carry〉
183      | _ ⇒ Error … [MSG UnsupportedOp]
184      ]
185    | _ ⇒ Error … [MSG UnsupportedOp]
186    ]
187  | BVnull p1 ⇒
188    match op with
189    [ Xor ⇒
190      match a2 with
191      [ BVptr _ p2 _ ⇒
192        if eqb p1 p2 then
193          return 〈BVnonzero, carry〉
194        else
195          Error … [MSG UnsupportedOp]
196      | BVnull p2 ⇒
197        if eqb p1 p2 then
198          return 〈BVByte (bv_zero …), carry〉
199        else
200          Error … [MSG UnsupportedOp]
201      | _ ⇒ Error … [MSG UnsupportedOp]
202      ]
203    | _ ⇒ Error … [MSG UnsupportedOp]
204    ]
205  | _ ⇒ Error … [MSG UnsupportedOp]
206  ].
207
Note: See TracBrowser for help on using the repository browser.