source: extracted/joint_LTL_LIN_semantics.ml @ 2829

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

Semantics files committed.

File size: 6.0 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open BitVectorTrie
12
13open Graphs
14
15open I8051
16
17open Order
18
19open Registers
20
21open CostLabel
22
23open Hide
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Lists
40
41open Identifiers
42
43open Integers
44
45open AST
46
47open Division
48
49open Exp
50
51open Arithmetic
52
53open Setoids
54
55open Monad
56
57open Option
58
59open Extranat
60
61open Vector
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open List
70
71open Util
72
73open FoldStuff
74
75open BitVector
76
77open Types
78
79open Bool
80
81open Relations
82
83open Nat
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107open Joint_LTL_LIN
108
109open ExtraMonads
110
111open Deqsets_extra
112
113open State
114
115open Bind_new
116
117open BindLists
118
119open Blocks
120
121open TranslateUtils
122
123open ExtraGlobalenvs
124
125open I8051bis
126
127open BEMem
128
129open Events
130
131open IOMonad
132
133open IO
134
135open Extra_bool
136
137open Coqlib
138
139open Values
140
141open FrontEndVal
142
143open GenMem
144
145open FrontEndMem
146
147open Globalenvs
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 -> Values.val0 List.list
194    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 lTL_LIN_semantics : 'a1 Joint_semantics.sem_unserialized_params **)
224let lTL_LIN_semantics =
225  { Joint_semantics.st_pars = lTL_LIN_state; Joint_semantics.acca_store_ =
226    (fun x -> Obj.magic (hw_reg_store I8051.RegisterA));
227    Joint_semantics.acca_retrieve_ = (fun e x ->
228    hw_reg_retrieve (Obj.magic e) I8051.RegisterA);
229    Joint_semantics.acca_arg_retrieve_ = (fun e x ->
230    hw_reg_retrieve (Obj.magic e) I8051.RegisterA);
231    Joint_semantics.accb_store_ = (fun x ->
232    Obj.magic (hw_reg_store I8051.RegisterB));
233    Joint_semantics.accb_retrieve_ = (fun e x ->
234    hw_reg_retrieve (Obj.magic e) I8051.RegisterB);
235    Joint_semantics.accb_arg_retrieve_ = (fun e x ->
236    hw_reg_retrieve (Obj.magic e) I8051.RegisterB);
237    Joint_semantics.dpl_store_ = (fun x ->
238    Obj.magic (hw_reg_store I8051.RegisterDPL));
239    Joint_semantics.dpl_retrieve_ = (fun e x ->
240    hw_reg_retrieve (Obj.magic e) I8051.RegisterDPL);
241    Joint_semantics.dpl_arg_retrieve_ = (fun e x ->
242    hw_reg_retrieve (Obj.magic e) I8051.RegisterDPL);
243    Joint_semantics.dph_store_ = (fun x ->
244    Obj.magic (hw_reg_store I8051.RegisterDPH));
245    Joint_semantics.dph_retrieve_ = (fun e x ->
246    hw_reg_retrieve (Obj.magic e) I8051.RegisterDPH);
247    Joint_semantics.dph_arg_retrieve_ = (fun e x ->
248    hw_reg_retrieve (Obj.magic e) I8051.RegisterDPH);
249    Joint_semantics.snd_arg_retrieve_ = (Obj.magic hw_arg_retrieve);
250    Joint_semantics.pair_reg_move_ = (Obj.magic eval_registers_move);
251    Joint_semantics.save_frame = (Obj.magic lTL_LIN_save_frame);
252    Joint_semantics.setup_call = (fun x x0 x1 st ->
253    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st));
254    Joint_semantics.fetch_external_args = (assert false (* absurd case *));
255    Joint_semantics.set_result = (Obj.magic ltl_lin_set_result);
256    Joint_semantics.call_args_for_main = (Obj.magic Nat.O);
257    Joint_semantics.call_dest_for_main = (Obj.magic Types.It);
258    Joint_semantics.read_result = (fun x x0 x1 st ->
259    Obj.magic
260      (Monad.m_return0 (Monad.max_def Errors.res0)
261        (List.map
262          (SemanticsUtils.hwreg_retrieve (Obj.magic st.Joint_semantics.regs))
263          I8051.registerRets))); Joint_semantics.eval_ext_seq = (assert false
264    (* absurd case *)); Joint_semantics.pop_frame = (fun x x0 x1 x2 st ->
265    Joint_semantics.pop_ra lTL_LIN_state st) }
266
Note: See TracBrowser for help on using the repository browser.