source: src/common/BackEndOps.ma @ 2541

Last change on this file since 2541 was 2462, checked in by tranquil, 7 years ago

separated in back end values program counters from code pointers (intended to hold function pointers only): same signature, but separation needed the proof of some passes
File size: 9.8 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 ptr p ⇒
69    match ptype ptr with
70    [ Code ⇒ Error … [MSG UnsupportedOp]
71    | XData ⇒
72      match p with
73      [ O ⇒
74        ! carry' ← Bit_of_val UnsupportedOp carry ;
75        if carry' then Error … [MSG UnsupportedOp]
76        else
77          let o1o0 : Byte × Byte ≝ vsplit ? 8 8 (offv (poff ptr)) in
78          let 〈rslt,carry〉 ≝ op2 eval false op b2 (\snd o1o0) in
79          let p0 ≝ mk_part 0 (le_S … (le_n …)) in
80          let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (\fst o1o0 @@ rslt)) in
81          return 〈BVptr ptr' p, BBptrcarry is_add ptr p0 b2〉
82      | _ ⇒ (* it is 1. To generalize, many casts ⌈…⌉ needs to be added *)
83        match carry with
84        [ BBptrcarry is_add' ptr' p' by' ⇒
85          if eq_b is_add is_add' ∧ eq_block (pblock ptr) (pblock ptr') ∧
86            eq_bv_suffix 8 8 8 (offv (poff ptr)) (offv (poff ptr'))
87          then If eqb p' 0 then with prf do
88            let by' : Byte ≝ by' ⌈? ↦ Byte⌉ in
89            let o1o0 ≝ vsplit ? 8 8 (offv (poff ptr)) in
90            let o1o0 ≝ [[\fst o1o0 ; \snd o1o0]] in
91            let 〈rslt,ignore〉 ≝ op2_bytes op ? false o1o0 [[b2 ; by']] in
92            let part1 ≝ mk_part 1 (le_n …) in
93            let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (vflatten … rslt)) in
94            OK … 〈BVptr ptr' part1,
95                  BBptrcarry is_add ptr' part1 (b2 @@ by')〉
96          else Error … [MSG UnsupportedOp]
97          else Error … [MSG UnsupportedOp]
98        | _ ⇒ Error … [MSG UnsupportedOp]
99        ]
100      ]
101    ]
102  | _ ⇒ Error … [MSG UnsupportedOp]
103  ].
104@hide_prf
105lapply prf @(eqb_elim p') #H * >H %
106qed.
107
108definition byte_at : ∀n.BitVector (8*n) → ∀p.p < n → Byte ≝
109λn,v,p,H.
110let suffix : BitVector (8 + 8*p) ≝
111  \snd (vsplit … (v⌈BitVector ?↦BitVector (8*(n - S p) + (8 + 8*p))⌉)) in
112\fst (vsplit … suffix).
113>(commutative_times_fast ? p)
114change with (? = BitVector (? + S p*8))
115>(commutative_times_fast (S p))
116<distributive_times_plus_fast
117<(plus_minus_m_m … H) %
118qed.
119
120definition eq_opt : ∀A.(A → A → bool) → option A → option A → bool ≝
121λA,eq,m,n.
122match m with
123[ Some a ⇒
124  match n with
125  [ Some b ⇒ eq a b
126  | _ ⇒ false
127  ]
128| _ ⇒
129  match m with
130  [ None ⇒ true
131  | _ ⇒ false
132  ]
133].
134
135(* This tables shows what binary ops may be defined on bevals depending on
136   the arguments (columns marked by 1st argument, rows by 2nd). Further
137   checks for definedness are done for pointer parts taking into account
138   blocks, parts and the carry value.
139   Neither BVundef nor BVpc allow any operations
140  arg2\arg1 | BVByte    | BVptr (D)      | BVptr (C) | BVnull | BVXor | BVnonzero |
141  ----------+-----------+----------------+-----------+--------+-------+-----------+
142  BVByte    | all       | Add, Addc, Sub | --        | --     | --    | Or        |
143  ----------+-----------+----------------+-----------+--------+-------+-----------+
144  BVptr (D) | Add, Addc | Sub, Xor       | Xor       | Xor    | --    | --        |
145  ----------+-----------+----------------+-----------+--------+-------+-----------+
146  BVptr (C) | --        | Xor            | Xor       | Xor    | --    | --        |
147  ----------+-----------+----------------+-----------+--------+-------+-----------+
148  BVnull    | --        | Xor            | Xor       | Xor    | --    | --        |
149  ----------+-----------+----------------+-----------+--------+-------+-----------+
150  BVXor     | --        | --             | --        | --     | Or    | Or        |
151  ----------+-----------+----------------+-----------+--------+-------+-----------+
152  BVnonzero | Or        | --             | --        | --     | Or    | --        |
153  ----------+-----------+----------------+-----------+--------+-------+-----------+
154*)
155definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝
156  λcarry,op,a1,a2.
157  match a1 with
158  [ BVByte b1 ⇒
159(*    if match op with [ Or ⇒ true | _ ⇒ false ] ∧ eq_bv … (zero …) b1 then
160      return 〈a2, carry〉
161    else *) (* maybe it will be needed, need to see actual translations *)
162      match a2 with
163      [ BVByte b2 ⇒
164        ! carry ← Bit_of_val UnsupportedOp carry ;
165        let 〈result, carry〉 ≝ op2 eval carry op b1 b2 in
166        return 〈BVByte result, BBbit carry〉
167      | BVptr _ _ ⇒
168        match op with
169        [ Add ⇒ be_add_sub_byte true (BBbit false) a2 b1
170        | Addc ⇒ be_add_sub_byte true carry a2 b1
171        | _ ⇒ Error … [MSG UnsupportedOp]
172        ]
173      | BVnonzero ⇒
174        match op with
175        [ Or ⇒ return 〈BVnonzero, carry〉
176        | _ ⇒ Error … [MSG UnsupportedOp]
177        ]
178      | _ ⇒ Error … [MSG UnsupportedOp]
179      ]
180  | BVptr ptr1 p1 ⇒
181    match a2 with
182    [ BVByte b2 ⇒
183      match op with
184      [ Add ⇒ be_add_sub_byte true (BBbit false) a1 b2
185      | Addc ⇒ be_add_sub_byte true carry a1 b2
186      | Sub ⇒ be_add_sub_byte false carry a1 b2
187      | _ ⇒ Error … [MSG UnsupportedOp]
188      ]
189    | BVptr ptr2 p2 ⇒
190      match op with
191      [ Sub ⇒
192        match ptype ptr1 with
193        [ Code ⇒ Error … [MSG UnsupportedOp]
194        | XData ⇒
195          if eq_block (pblock ptr1) (pblock ptr2) ∧
196             eqb p1 p2
197          then
198          ! carry ← Bit_of_val UnsupportedOp carry ;
199            let by1 ≝ byte_at ? (offv (poff ptr1)) … (part_no_ok p1) in
200            let by2 ≝ byte_at ? (offv (poff ptr2)) … (part_no_ok p1) in
201            let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in
202            return 〈BVByte result, BBbit carry〉
203          else Error … [MSG UnsupportedOp]
204        ]
205      | Xor ⇒
206        if eqb p1 p2 then
207          return 〈BVXor (Some ? ptr1) (Some ? ptr2) p1, carry〉
208        else Error … [MSG UnsupportedOp]
209      | _ ⇒ Error … [MSG UnsupportedOp]
210      ]
211    | BVnull p2 ⇒
212      match op with
213      [ Xor ⇒
214        if eqb p1 p2 then
215          return 〈BVXor (Some ? ptr1) (None ?) p1, carry〉
216        else
217          Error … [MSG UnsupportedOp]
218      | _ ⇒ Error … [MSG UnsupportedOp]
219      ]
220    | _ ⇒ Error … [MSG UnsupportedOp]
221    ]
222  | BVnull p1 ⇒
223    match op with
224    [ Xor ⇒
225      match a2 with
226      [ BVptr ptr2 p2 ⇒
227        if eqb p1 p2 then
228          return 〈BVXor (None ?) (Some ? ptr2) p1, carry〉
229        else
230          Error … [MSG UnsupportedOp]
231      | BVnull p2 ⇒
232        if eqb p1 p2 then
233          return 〈BVXor (None ?) (None ?) p1, carry〉
234        else
235          Error … [MSG UnsupportedOp]
236      | _ ⇒ Error … [MSG UnsupportedOp]
237      ]
238    | _ ⇒ Error … [MSG UnsupportedOp]
239    ]
240  | BVXor ptr1_opt ptr1_opt' p1 ⇒
241    match op with
242    [ Or ⇒
243      match a2 with
244      [ BVByte b2 ⇒
245        if eq_bv … (bv_zero …) b2 then return 〈a1, carry〉
246        else Error … [MSG UnsupportedOp]
247      | BVnonzero ⇒ return 〈BVnonzero, carry〉
248      | BVXor ptr2_opt ptr2_opt' p2 ⇒
249        if ((eqb p1 0 ∧ eqb p2 1) ∨ (eqb p1 1 ∧ eqb p2 0)) then
250          let eq_at ≝ λp,ptr1,ptr2.
251            eq_block (pblock ptr1) (pblock ptr2) ∧
252            eq_bv … (byte_at ? (offv (poff ptr1)) … (part_no_ok p))
253                    (byte_at ? (offv (poff ptr2)) … (part_no_ok p)) in
254          if eq_opt ? (eq_at p1) ptr1_opt ptr1_opt' ∧
255             eq_opt ? (eq_at p2) ptr2_opt ptr2_opt'
256          then return 〈BVByte (bv_zero …), carry〉
257          else return 〈BVnonzero, carry〉
258        else Error … [MSG UnsupportedOp]
259      | _ ⇒ Error … [MSG UnsupportedOp]
260      ]
261    | _ ⇒ Error … [MSG UnsupportedOp]
262    ]
263  | BVnonzero ⇒
264    match op with
265    [ Or ⇒
266      match a2 with
267      [ BVByte _ ⇒ return 〈BVnonzero, carry〉
268      | BVnonzero ⇒ return 〈BVnonzero, carry〉
269      | BVXor _ _ _ ⇒ return 〈BVnonzero, carry〉
270      | _ ⇒ Error … [MSG UnsupportedOp]
271      ]
272    | _ ⇒ Error … [MSG UnsupportedOp]
273    ]
274  | _ ⇒ Error … [MSG UnsupportedOp]
275  ].
Note: See TracBrowser for help on using the repository browser.