source: driver/extracted/joint_LTL_LIN_semantics.ml

Last change on this file was 3043, checked in by sacerdot, 7 years ago

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 8.5 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open GenMem
12
13open FrontEndMem
14
15open Globalenvs
16
17open String
18
19open Sets
20
21open Listb
22
23open LabelledObjects
24
25open BitVectorTrie
26
27open Graphs
28
29open I8051
30
31open Order
32
33open Registers
34
35open CostLabel
36
37open Hide
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Exp
64
65open Arithmetic
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open Div_and_mod
78
79open Jmeq
80
81open Russell
82
83open List
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Types
92
93open Bool
94
95open Relations
96
97open Nat
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Positive
108
109open Z
110
111open BitVectorZ
112
113open Pointers
114
115open ByteValues
116
117open BackEndOps
118
119open Joint
120
121open Joint_LTL_LIN
122
123open ExtraMonads
124
125open Deqsets_extra
126
127open State
128
129open Bind_new
130
131open BindLists
132
133open Blocks
134
135open TranslateUtils
136
137open ExtraGlobalenvs
138
139open I8051bis
140
141open BEMem
142
143open Events
144
145open IOMonad
146
147open IO
148
149open Joint_semantics
150
151open SemanticsUtils
152
153(** val hw_reg_store :
154    I8051.register -> ByteValues.beval -> SemanticsUtils.hw_register_env ->
155    SemanticsUtils.hw_register_env Errors.res **)
156let hw_reg_store r v e =
157  Errors.OK (SemanticsUtils.hwreg_store r v e)
158
159(** val hw_reg_retrieve :
160    SemanticsUtils.hw_register_env -> I8051.register -> ByteValues.beval
161    Errors.res **)
162let hw_reg_retrieve l r =
163  Errors.OK (SemanticsUtils.hwreg_retrieve l r)
164
165(** val hw_arg_retrieve :
166    SemanticsUtils.hw_register_env -> I8051.register Joint.argument ->
167    ByteValues.beval Errors.res **)
168let hw_arg_retrieve l = function
169| Joint.Reg r -> hw_reg_retrieve l r
170| Joint.Imm b -> Errors.OK (ByteValues.BVByte b)
171
172(** val eval_registers_move :
173    SemanticsUtils.hw_register_env -> Joint_LTL_LIN.registers_move ->
174    SemanticsUtils.hw_register_env Errors.res **)
175let eval_registers_move e = function
176| Joint_LTL_LIN.From_acc (r, x) ->
177  hw_reg_store r (SemanticsUtils.hwreg_retrieve e I8051.RegisterA) e
178| Joint_LTL_LIN.To_acc (x, r) ->
179  hw_reg_store I8051.RegisterA (SemanticsUtils.hwreg_retrieve e r) e
180| Joint_LTL_LIN.Int_to_reg (r, v) -> hw_reg_store r (ByteValues.BVByte v) e
181| Joint_LTL_LIN.Int_to_acc (x, v) ->
182  hw_reg_store I8051.RegisterA (ByteValues.BVByte v) e
183
184(** val lTL_LIN_state : Joint_semantics.sem_state_params **)
185let lTL_LIN_state =
186  { Joint_semantics.empty_framesT = (Obj.magic Types.It);
187    Joint_semantics.empty_regsT =
188    (Obj.magic SemanticsUtils.init_hw_register_env);
189    Joint_semantics.load_sp = (Obj.magic SemanticsUtils.hwreg_retrieve_sp);
190    Joint_semantics.save_sp = (Obj.magic SemanticsUtils.hwreg_store_sp) }
191
192(** val ltl_lin_fetch_external_args :
193    AST.external_function -> Joint_semantics.state -> Nat.nat -> Values.val0
194    List.list Errors.res **)
195let ltl_lin_fetch_external_args _ =
196  failwith "AXIOM TO BE REALIZED"
197
198(** val ltl_lin_set_result :
199    Values.val0 List.list -> Types.unit0 -> Joint_semantics.state ->
200    Joint_semantics.state Errors.res **)
201let ltl_lin_set_result _ =
202  failwith "AXIOM TO BE REALIZED"
203
204(** val lTL_LIN_save_frame :
205    Joint_semantics.call_kind -> Types.unit0 -> Joint_semantics.state_pc ->
206    Joint_semantics.state Errors.res **)
207let lTL_LIN_save_frame k x st =
208  match k with
209  | Joint_semantics.PTR ->
210    Obj.magic
211      (Monad.m_bind0 (Monad.max_def Errors.res0)
212        (Obj.magic
213          (ByteValues.byte_of_val ErrorMessages.BadFunction
214            (SemanticsUtils.hwreg_retrieve
215              (Obj.magic st.Joint_semantics.st_no_pc.Joint_semantics.regs)
216              I8051.RegisterA))) (fun v ->
217        match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
218                (Nat.S (Nat.S Nat.O)))))))) v
219                (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
220                  (Nat.S (Nat.S Nat.O))))))))) with
221        | Bool.True ->
222          Monad.m_return0 (Monad.max_def Errors.res0)
223            st.Joint_semantics.st_no_pc
224        | Bool.False ->
225          Obj.magic (Errors.Error (List.Cons ((Errors.MSG
226            ErrorMessages.BadFunction), (List.Cons ((Errors.MSG
227            ErrorMessages.BadPointer), List.Nil)))))))
228  | Joint_semantics.ID ->
229    Joint_semantics.push_ra lTL_LIN_state st.Joint_semantics.st_no_pc
230      st.Joint_semantics.pc
231
232(** val eval_LTL_LIN_ext_seq :
233    AST.ident List.list -> 'a1 Joint_semantics.genv_gen ->
234    Joint_LTL_LIN.ltl_lin_seq -> AST.ident -> Joint_semantics.state ->
235    Joint_semantics.state Errors.res **)
236let eval_LTL_LIN_ext_seq globals ge s curr_id st =
237  match s with
238  | Joint_LTL_LIN.SAVE_CARRY ->
239    let regs =
240      SemanticsUtils.hwreg_set_other st.Joint_semantics.carry
241        (Obj.magic st.Joint_semantics.regs)
242    in
243    Obj.magic
244      (Monad.m_return0 (Monad.max_def Errors.res0)
245        (Joint_semantics.set_regs lTL_LIN_state (Obj.magic regs) st))
246  | Joint_LTL_LIN.RESTORE_CARRY ->
247    let carry = (Obj.magic st.Joint_semantics.regs).SemanticsUtils.other_bit
248    in
249    Obj.magic
250      (Monad.m_return0 (Monad.max_def Errors.res0)
251        (Joint_semantics.set_carry lTL_LIN_state carry st))
252  | Joint_LTL_LIN.LOW_ADDRESS l ->
253    Obj.magic
254      (Monad.m_bind0 (Monad.max_def Errors.res0)
255        (Obj.magic (Joint_semantics.gen_pc_from_label globals ge curr_id l))
256        (fun pc_lab ->
257        let { Types.fst = addrl; Types.snd = addrh } =
258          ByteValues.beval_pair_of_pc pc_lab
259        in
260        let regs =
261          SemanticsUtils.hwreg_store I8051.RegisterA addrl
262            (Obj.magic st.Joint_semantics.regs)
263        in
264        Monad.m_return0 (Monad.max_def Errors.res0)
265          (Joint_semantics.set_regs lTL_LIN_state (Obj.magic regs) st)))
266  | Joint_LTL_LIN.HIGH_ADDRESS l ->
267    Obj.magic
268      (Monad.m_bind0 (Monad.max_def Errors.res0)
269        (Obj.magic (Joint_semantics.gen_pc_from_label globals ge curr_id l))
270        (fun pc_lab ->
271        let { Types.fst = addrl; Types.snd = addrh } =
272          ByteValues.beval_pair_of_pc pc_lab
273        in
274        let regs =
275          SemanticsUtils.hwreg_store I8051.RegisterA addrh
276            (Obj.magic st.Joint_semantics.regs)
277        in
278        Monad.m_return0 (Monad.max_def Errors.res0)
279          (Joint_semantics.set_regs lTL_LIN_state (Obj.magic regs) st)))
280
281(** val lTL_LIN_semantics : 'a1 Joint_semantics.sem_unserialized_params **)
282let lTL_LIN_semantics =
283  { Joint_semantics.st_pars = lTL_LIN_state; Joint_semantics.acca_store_ =
284    (fun x -> Obj.magic (hw_reg_store I8051.RegisterA));
285    Joint_semantics.acca_retrieve_ = (fun e x ->
286    hw_reg_retrieve (Obj.magic e) I8051.RegisterA);
287    Joint_semantics.acca_arg_retrieve_ = (fun e x ->
288    hw_reg_retrieve (Obj.magic e) I8051.RegisterA);
289    Joint_semantics.accb_store_ = (fun x ->
290    Obj.magic (hw_reg_store I8051.RegisterB));
291    Joint_semantics.accb_retrieve_ = (fun e x ->
292    hw_reg_retrieve (Obj.magic e) I8051.RegisterB);
293    Joint_semantics.accb_arg_retrieve_ = (fun e x ->
294    hw_reg_retrieve (Obj.magic e) I8051.RegisterB);
295    Joint_semantics.dpl_store_ = (fun x ->
296    Obj.magic (hw_reg_store I8051.RegisterDPL));
297    Joint_semantics.dpl_retrieve_ = (fun e x ->
298    hw_reg_retrieve (Obj.magic e) I8051.RegisterDPL);
299    Joint_semantics.dpl_arg_retrieve_ = (fun e x ->
300    hw_reg_retrieve (Obj.magic e) I8051.RegisterDPL);
301    Joint_semantics.dph_store_ = (fun x ->
302    Obj.magic (hw_reg_store I8051.RegisterDPH));
303    Joint_semantics.dph_retrieve_ = (fun e x ->
304    hw_reg_retrieve (Obj.magic e) I8051.RegisterDPH);
305    Joint_semantics.dph_arg_retrieve_ = (fun e x ->
306    hw_reg_retrieve (Obj.magic e) I8051.RegisterDPH);
307    Joint_semantics.snd_arg_retrieve_ = (Obj.magic hw_arg_retrieve);
308    Joint_semantics.pair_reg_move_ = (Obj.magic eval_registers_move);
309    Joint_semantics.save_frame = (Obj.magic lTL_LIN_save_frame);
310    Joint_semantics.setup_call = (fun x x0 x1 st ->
311    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st));
312    Joint_semantics.fetch_external_args =
313    (Obj.magic ltl_lin_fetch_external_args); Joint_semantics.set_result =
314    (Obj.magic ltl_lin_set_result); Joint_semantics.call_args_for_main =
315    (Obj.magic Nat.O); Joint_semantics.call_dest_for_main =
316    (Obj.magic Types.It); Joint_semantics.read_result = (fun x x0 x1 st ->
317    Obj.magic
318      (Monad.m_return0 (Monad.max_def Errors.res0)
319        (List.map
320          (SemanticsUtils.hwreg_retrieve (Obj.magic st.Joint_semantics.regs))
321          I8051.registerRets))); Joint_semantics.eval_ext_seq =
322    (Obj.magic eval_LTL_LIN_ext_seq); Joint_semantics.pop_frame =
323    (fun x x0 x1 x2 st -> Joint_semantics.pop_ra lTL_LIN_state st) }
324
Note: See TracBrowser for help on using the repository browser.