source: extracted/joint_LTL_LIN_semantics.ml @ 2997

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

New extraction.

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