source: src/common/BackEndOps.ma @ 2645

Last change on this file since 2645 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 10.2 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
38definition be_opaccs : OpAccs → beval → beval → res (beval × beval) ≝
39  λop,a,b.
40  ! a' ← Byte_of_val UnsupportedOp a ;
41  ! b' ← Byte_of_val UnsupportedOp b ;
42  let 〈a'',b''〉 ≝ opaccs eval op a' b' in
43  return 〈BVByte a'', BVByte b''〉.
44
45definition be_op1 : Op1 → beval → res beval ≝
46  λop,a.
47  ! a' ← Byte_of_val UnsupportedOp a ;
48  return BVByte (op1 eval op a').
49
50definition op2_bytes : Op2 → ∀n.Bit → Vector Byte n → Vector Byte n → (Vector Byte n) × Bit ≝
51λop,n,carry.
52  let f ≝ λn,b1,b2.λpr : (Vector Byte n) × Bit.
53    let 〈res_tl, carry〉 ≝ pr in
54    let 〈res_hd,carry'〉 ≝ op2 eval carry op b1 b2 in
55    〈res_hd ::: res_tl, carry'〉 in
56  fold_right2_i … f 〈[[ ]],carry〉 n.
57
58definition be_add_sub_byte : bool → bebit → beval → Byte → res (beval × bebit) ≝
59  λis_add,carry,a1,b2.
60  let op ≝ if is_add then Addc else Sub in
61  match a1 with
62  [ BVByte b1 ⇒
63    ! carry' ← Bit_of_val UnsupportedOp carry ;
64    let 〈rslt, carry''〉 ≝ op2 eval carry' op b1 b2 in
65    return 〈BVByte rslt, BBbit carry''〉
66  | BVptr ptr p ⇒
67    match ptype ptr with
68    [ Code ⇒ Error … [MSG UnsupportedOp]
69    | XData ⇒
70      match p with
71      [ O ⇒
72        ! carry' ← Bit_of_val UnsupportedOp carry ;
73        if carry' then Error … [MSG UnsupportedOp]
74        else
75          let o1o0 : Byte × Byte ≝ vsplit ? 8 8 (offv (poff ptr)) in
76          let 〈rslt,carry〉 ≝ op2 eval false op b2 (\snd o1o0) in
77          let p0 ≝ mk_part 0 (le_S … (le_n …)) in
78          let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (\fst o1o0 @@ rslt)) in
79          return 〈BVptr ptr' p, BBptrcarry is_add ptr p0 b2〉
80      | _ ⇒ (* it is 1. To generalize, many casts ⌈…⌉ needs to be added *)
81        match carry with
82        [ BBptrcarry is_add' ptr' p' by' ⇒
83          if eq_b is_add is_add' ∧ eq_block (pblock ptr) (pblock ptr') ∧
84            eq_bv_suffix 8 8 8 (offv (poff ptr)) (offv (poff ptr'))
85          then If eqb p' 0 then with prf do
86            let by' : Byte ≝ by' ⌈? ↦ Byte⌉ in
87            let o1o0 ≝ vsplit ? 8 8 (offv (poff ptr)) in
88            let o1o0 ≝ [[\fst o1o0 ; \snd o1o0]] in
89            let 〈rslt,ignore〉 ≝ op2_bytes op ? false o1o0 [[b2 ; by']] in
90            let part1 ≝ mk_part 1 (le_n …) in
91            let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (vflatten … rslt)) in
92            OK … 〈BVptr ptr' part1,
93                  BBptrcarry is_add ptr' part1 (b2 @@ by')〉
94          else Error … [MSG UnsupportedOp]
95          else Error … [MSG UnsupportedOp]
96        | _ ⇒ Error … [MSG UnsupportedOp]
97        ]
98      ]
99    ]
100  | _ ⇒ Error … [MSG UnsupportedOp]
101  ].
102@hide_prf
103lapply prf @(eqb_elim p') #H * >H %
104qed.
105
106definition byte_at : ∀n.BitVector (8*n) → ∀p.p < n → Byte ≝
107λn,v,p,H.
108let suffix : BitVector (8 + 8*p) ≝
109  \snd (vsplit … (v⌈BitVector ?↦BitVector (8*(n - S p) + (8 + 8*p))⌉)) in
110\fst (vsplit … suffix).
111>(commutative_times_fast ? p)
112change with (? = BitVector (? + S p*8))
113>(commutative_times_fast (S p))
114<distributive_times_plus_fast
115<(plus_minus_m_m … H) %
116qed.
117
118definition eq_opt : ∀A.(A → A → bool) → option A → option A → bool ≝
119λA,eq,m,n.
120match m with
121[ Some a ⇒
122  match n with
123  [ Some b ⇒ eq a b
124  | _ ⇒ false
125  ]
126| _ ⇒
127  match m with
128  [ None ⇒ true
129  | _ ⇒ false
130  ]
131].
132
133(* This tables shows what binary ops may be defined on bevals depending on
134   the arguments (columns marked by 1st argument, rows by 2nd). Further
135   checks for definedness are done for pointer parts taking into account
136   blocks, parts and the carry value.
137   Neither BVundef nor BVpc allow any operations
138  arg2\arg1 | BVByte    | BVptr (D)      | BVptr (C) | BVnull | BVXor | BVnonzero |
139  ----------+-----------+----------------+-----------+--------+-------+-----------+
140  BVByte    | all       | Add, Addc, Sub | --        | --     | --    | Or        |
141  ----------+-----------+----------------+-----------+--------+-------+-----------+
142  BVptr (D) | Add, Addc | Sub, Xor       | Xor       | Xor    | --    | --        |
143  ----------+-----------+----------------+-----------+--------+-------+-----------+
144  BVptr (C) | --        | Xor            | Xor       | Xor    | --    | --        |
145  ----------+-----------+----------------+-----------+--------+-------+-----------+
146  BVnull    | --        | Xor            | Xor       | Xor    | --    | --        |
147  ----------+-----------+----------------+-----------+--------+-------+-----------+
148  BVXor     | --        | --             | --        | --     | Or    | Or        |
149  ----------+-----------+----------------+-----------+--------+-------+-----------+
150  BVnonzero | Or        | --             | --        | --     | Or    | --        |
151  ----------+-----------+----------------+-----------+--------+-------+-----------+
152*)
153definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝
154  λcarry,op,a1,a2.
155  match a1 with
156  [ BVByte b1 ⇒
157(*    if match op with [ Or ⇒ true | _ ⇒ false ] ∧ eq_bv … (zero …) b1 then
158      return 〈a2, carry〉
159    else *) (* maybe it will be needed, need to see actual translations *)
160      match a2 with
161      [ BVByte b2 ⇒
162        ! carry ← Bit_of_val UnsupportedOp carry ;
163        let 〈result, carry〉 ≝ op2 eval carry op b1 b2 in
164        return 〈BVByte result, BBbit carry〉
165      | BVptr _ _ ⇒
166        match op with
167        [ Add ⇒ be_add_sub_byte true (BBbit false) a2 b1
168        | Addc ⇒ be_add_sub_byte true carry a2 b1
169        | _ ⇒ Error … [MSG UnsupportedOp]
170        ]
171      | BVnonzero ⇒
172        match op with
173        [ Or ⇒ return 〈BVnonzero, carry〉
174        | _ ⇒ Error … [MSG UnsupportedOp]
175        ]
176      | _ ⇒ Error … [MSG UnsupportedOp]
177      ]
178  | BVptr ptr1 p1 ⇒
179    match a2 with
180    [ BVByte b2 ⇒
181      match op with
182      [ Add ⇒ be_add_sub_byte true (BBbit false) a1 b2
183      | Addc ⇒ be_add_sub_byte true carry a1 b2
184      | Sub ⇒ be_add_sub_byte false carry a1 b2
185      | _ ⇒ Error … [MSG UnsupportedOp]
186      ]
187    | BVptr ptr2 p2 ⇒
188      match op with
189      [ Sub ⇒
190        match ptype ptr1 with
191        [ Code ⇒ Error … [MSG UnsupportedOp]
192        | XData ⇒
193          if eq_block (pblock ptr1) (pblock ptr2) ∧
194             eqb p1 p2
195          then
196          ! carry ← Bit_of_val UnsupportedOp carry ;
197            let by1 ≝ byte_at ? (offv (poff ptr1)) … (part_no_ok p1) in
198            let by2 ≝ byte_at ? (offv (poff ptr2)) … (part_no_ok p1) in
199            let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in
200            return 〈BVByte result, BBbit carry〉
201          else Error … [MSG UnsupportedOp]
202        ]
203      | Xor ⇒
204        if eqb p1 p2 then
205          return 〈BVXor (Some ? ptr1) (Some ? ptr2) p1, carry〉
206        else Error … [MSG UnsupportedOp]
207      | _ ⇒ Error … [MSG UnsupportedOp]
208      ]
209    | BVnull p2 ⇒
210      match op with
211      [ Xor ⇒
212        if eqb p1 p2 then
213          return 〈BVXor (Some ? ptr1) (None ?) p1, carry〉
214        else
215          Error … [MSG UnsupportedOp]
216      | _ ⇒ Error … [MSG UnsupportedOp]
217      ]
218    | _ ⇒ Error … [MSG UnsupportedOp]
219    ]
220  | BVnull p1 ⇒
221    match a2 with
222    [ BVptr ptr2 p2 ⇒
223      match op with
224      [ Xor ⇒
225        if eqb p1 p2 then
226          return 〈BVXor (None ?) (Some ? ptr2) p1, carry〉
227        else
228          Error … [MSG UnsupportedOp]
229      | _ ⇒ Error … [MSG UnsupportedOp]
230      ]
231    | BVnull p2 ⇒
232      match op with
233      [ Xor ⇒
234        if eqb p1 p2 then
235          return 〈BVXor (None ?) (None ?) p1, carry〉
236        else
237          Error … [MSG UnsupportedOp]
238      | _ ⇒ Error … [MSG UnsupportedOp]
239      ]
240    | _ ⇒ Error … [MSG UnsupportedOp]
241    ]
242  | BVXor ptr1_opt ptr1_opt' p1 ⇒
243    match a2 with
244    [ BVByte b2 ⇒
245      match op with
246      [ Or ⇒
247        if eq_bv … (bv_zero …) b2 then return 〈a1, carry〉
248        else Error … [MSG UnsupportedOp]
249      | _ ⇒ Error … [MSG UnsupportedOp]
250      ]
251    | BVnonzero ⇒
252      match op with
253      [ Or ⇒
254        return 〈BVnonzero, carry〉
255      | _ ⇒ Error … [MSG UnsupportedOp]
256      ]
257    | BVXor ptr2_opt ptr2_opt' p2 ⇒
258      match op with
259      [ Or ⇒
260        if ((eqb p1 0 ∧ eqb p2 1) ∨ (eqb p1 1 ∧ eqb p2 0)) then
261          let eq_at ≝ λp,ptr1,ptr2.
262            eq_block (pblock ptr1) (pblock ptr2) ∧
263            eq_bv … (byte_at ? (offv (poff ptr1)) … (part_no_ok p))
264                    (byte_at ? (offv (poff ptr2)) … (part_no_ok p)) in
265          if eq_opt ? (eq_at p1) ptr1_opt ptr1_opt' ∧
266             eq_opt ? (eq_at p2) ptr2_opt ptr2_opt'
267          then return 〈BVByte (bv_zero …), carry〉
268          else return 〈BVnonzero, carry〉
269        else Error … [MSG UnsupportedOp]
270      | _ ⇒ Error … [MSG UnsupportedOp]
271      ]
272    | _ ⇒ Error … [MSG UnsupportedOp]
273    ]
274  | BVnonzero ⇒
275    match a2 with
276    [ BVByte _ ⇒
277      match op with
278      [ Or ⇒ return 〈BVnonzero, carry〉
279      | _ ⇒ Error … [MSG UnsupportedOp]
280      ]
281    | BVnonzero ⇒
282      match op with
283      [ Or ⇒ return 〈BVnonzero, carry〉
284      | _ ⇒ Error … [MSG UnsupportedOp]
285      ]
286    | BVXor _ _ _ ⇒
287      match op with
288      [ Or ⇒ return 〈BVnonzero, carry〉
289      | _ ⇒ Error … [MSG UnsupportedOp]
290      ]
291    | _ ⇒ Error … [MSG UnsupportedOp]
292    ]
293  | _ ⇒ Error … [MSG UnsupportedOp]
294  ].
Note: See TracBrowser for help on using the repository browser.