source: extracted/joint_LTL_LIN_semantics.ml @ 2960

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

New extraction, it diverges in RTL execution now.

File size: 7.9 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 eval_ltl_lin_seq :
205    Joint_LTL_LIN.ltl_lin_seq -> Joint_semantics.state -> (IO.io_out,
206    IO.io_in, Joint_semantics.state) IOMonad.iO **)
207let eval_ltl_lin_seq _ =
208  failwith "AXIOM TO BE REALIZED"
209
210(** val lTL_LIN_save_frame :
211    Joint_semantics.call_kind -> Types.unit0 -> Joint_semantics.state_pc ->
212    Joint_semantics.state Errors.res **)
213let lTL_LIN_save_frame k x st =
214  match k with
215  | Joint_semantics.PTR ->
216    Obj.magic
217      (Monad.m_return0 (Monad.max_def Errors.res0)
218        st.Joint_semantics.st_no_pc)
219  | Joint_semantics.ID ->
220    Joint_semantics.push_ra lTL_LIN_state st.Joint_semantics.st_no_pc
221      st.Joint_semantics.pc
222
223(** val eval_LTL_LIN_ext_seq :
224    AST.ident List.list -> 'a1 Joint_semantics.genv_gen ->
225    Joint_LTL_LIN.ltl_lin_seq -> AST.ident -> Joint_semantics.state ->
226    Joint_semantics.state Errors.res **)
227let eval_LTL_LIN_ext_seq globals ge s curr_id st =
228  match s with
229  | Joint_LTL_LIN.SAVE_CARRY ->
230    let regs =
231      SemanticsUtils.hwreg_set_other st.Joint_semantics.carry
232        (Obj.magic st.Joint_semantics.regs)
233    in
234    Obj.magic
235      (Monad.m_return0 (Monad.max_def Errors.res0)
236        (Joint_semantics.set_regs lTL_LIN_state (Obj.magic regs) st))
237  | Joint_LTL_LIN.RESTORE_CARRY ->
238    let carry = (Obj.magic st.Joint_semantics.regs).SemanticsUtils.other_bit
239    in
240    Obj.magic
241      (Monad.m_return0 (Monad.max_def Errors.res0)
242        (Joint_semantics.set_carry lTL_LIN_state carry st))
243  | Joint_LTL_LIN.LOW_ADDRESS (r, l) ->
244    Obj.magic
245      (Monad.m_bind0 (Monad.max_def Errors.res0)
246        (Obj.magic (Joint_semantics.gen_pc_from_label globals ge curr_id l))
247        (fun pc_lab ->
248        let { Types.fst = addrl; Types.snd = addrh } =
249          ByteValues.beval_pair_of_pc pc_lab
250        in
251        let regs =
252          SemanticsUtils.hwreg_store r addrl
253            (Obj.magic st.Joint_semantics.regs)
254        in
255        Monad.m_return0 (Monad.max_def Errors.res0)
256          (Joint_semantics.set_regs lTL_LIN_state (Obj.magic regs) st)))
257  | Joint_LTL_LIN.HIGH_ADDRESS (r, l) ->
258    Obj.magic
259      (Monad.m_bind0 (Monad.max_def Errors.res0)
260        (Obj.magic (Joint_semantics.gen_pc_from_label globals ge curr_id l))
261        (fun pc_lab ->
262        let { Types.fst = addrl; Types.snd = addrh } =
263          ByteValues.beval_pair_of_pc pc_lab
264        in
265        let regs =
266          SemanticsUtils.hwreg_store r addrh
267            (Obj.magic st.Joint_semantics.regs)
268        in
269        Monad.m_return0 (Monad.max_def Errors.res0)
270          (Joint_semantics.set_regs lTL_LIN_state (Obj.magic regs) st)))
271
272(** val lTL_LIN_semantics : 'a1 Joint_semantics.sem_unserialized_params **)
273let lTL_LIN_semantics =
274  { Joint_semantics.st_pars = lTL_LIN_state; Joint_semantics.acca_store_ =
275    (fun x -> Obj.magic (hw_reg_store I8051.RegisterA));
276    Joint_semantics.acca_retrieve_ = (fun e x ->
277    hw_reg_retrieve (Obj.magic e) I8051.RegisterA);
278    Joint_semantics.acca_arg_retrieve_ = (fun e x ->
279    hw_reg_retrieve (Obj.magic e) I8051.RegisterA);
280    Joint_semantics.accb_store_ = (fun x ->
281    Obj.magic (hw_reg_store I8051.RegisterB));
282    Joint_semantics.accb_retrieve_ = (fun e x ->
283    hw_reg_retrieve (Obj.magic e) I8051.RegisterB);
284    Joint_semantics.accb_arg_retrieve_ = (fun e x ->
285    hw_reg_retrieve (Obj.magic e) I8051.RegisterB);
286    Joint_semantics.dpl_store_ = (fun x ->
287    Obj.magic (hw_reg_store I8051.RegisterDPL));
288    Joint_semantics.dpl_retrieve_ = (fun e x ->
289    hw_reg_retrieve (Obj.magic e) I8051.RegisterDPL);
290    Joint_semantics.dpl_arg_retrieve_ = (fun e x ->
291    hw_reg_retrieve (Obj.magic e) I8051.RegisterDPL);
292    Joint_semantics.dph_store_ = (fun x ->
293    Obj.magic (hw_reg_store I8051.RegisterDPH));
294    Joint_semantics.dph_retrieve_ = (fun e x ->
295    hw_reg_retrieve (Obj.magic e) I8051.RegisterDPH);
296    Joint_semantics.dph_arg_retrieve_ = (fun e x ->
297    hw_reg_retrieve (Obj.magic e) I8051.RegisterDPH);
298    Joint_semantics.snd_arg_retrieve_ = (Obj.magic hw_arg_retrieve);
299    Joint_semantics.pair_reg_move_ = (Obj.magic eval_registers_move);
300    Joint_semantics.save_frame = (Obj.magic lTL_LIN_save_frame);
301    Joint_semantics.setup_call = (fun x x0 x1 st ->
302    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st));
303    Joint_semantics.fetch_external_args =
304    (Obj.magic ltl_lin_fetch_external_args); Joint_semantics.set_result =
305    (Obj.magic ltl_lin_set_result); Joint_semantics.call_args_for_main =
306    (Obj.magic Nat.O); Joint_semantics.call_dest_for_main =
307    (Obj.magic Types.It); Joint_semantics.read_result = (fun x x0 x1 st ->
308    Obj.magic
309      (Monad.m_return0 (Monad.max_def Errors.res0)
310        (List.map
311          (SemanticsUtils.hwreg_retrieve (Obj.magic st.Joint_semantics.regs))
312          I8051.registerRets))); Joint_semantics.eval_ext_seq =
313    (Obj.magic eval_LTL_LIN_ext_seq); Joint_semantics.pop_frame =
314    (fun x x0 x1 x2 st -> Joint_semantics.pop_ra lTL_LIN_state st) }
315
Note: See TracBrowser for help on using the repository browser.