source: extracted/eRTLptr_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: 6.0 KB
Line 
1open Preamble
2
3open ExtraMonads
4
5open Deqsets_extra
6
7open State
8
9open Bind_new
10
11open BindLists
12
13open Blocks
14
15open TranslateUtils
16
17open ExtraGlobalenvs
18
19open I8051bis
20
21open String
22
23open Sets
24
25open Listb
26
27open LabelledObjects
28
29open BitVectorTrie
30
31open Graphs
32
33open I8051
34
35open Order
36
37open Registers
38
39open BackEndOps
40
41open Joint
42
43open BEMem
44
45open CostLabel
46
47open Events
48
49open IOMonad
50
51open IO
52
53open Extra_bool
54
55open Coqlib
56
57open Values
58
59open FrontEndVal
60
61open Hide
62
63open ByteValues
64
65open Division
66
67open Z
68
69open BitVectorZ
70
71open Pointers
72
73open GenMem
74
75open FrontEndMem
76
77open Proper
78
79open PositiveMap
80
81open Deqsets
82
83open Extralib
84
85open Lists
86
87open Identifiers
88
89open Exp
90
91open Arithmetic
92
93open Vector
94
95open Div_and_mod
96
97open Util
98
99open FoldStuff
100
101open BitVector
102
103open Extranat
104
105open Integers
106
107open AST
108
109open ErrorMessages
110
111open Option
112
113open Setoids
114
115open Monad
116
117open Jmeq
118
119open Russell
120
121open Positive
122
123open PreIdentifiers
124
125open Bool
126
127open Relations
128
129open Nat
130
131open List
132
133open Hints_declaration
134
135open Core_notation
136
137open Pts
138
139open Logic
140
141open Types
142
143open Errors
144
145open Globalenvs
146
147open Joint_semantics
148
149open SemanticsUtils
150
151open ERTL
152
153open ERTLptr
154
155open ERTL_semantics
156
157(** val ertlptr_save_frame :
158    Joint_semantics.call_kind -> Types.unit0 -> Joint_semantics.state_pc ->
159    Joint_semantics.state Errors.res **)
160let ertlptr_save_frame k x st =
161  Obj.magic
162    (Monad.m_bind0 (Monad.max_def Errors.res0)
163      (match k with
164       | Joint_semantics.PTR ->
165         Monad.m_return0 (Monad.max_def Errors.res0)
166           (let x0 = st.Joint_semantics.st_no_pc in x0)
167       | Joint_semantics.ID ->
168         Obj.magic
169           (Joint_semantics.push_ra ERTL_semantics.eRTL_state
170             st.Joint_semantics.st_no_pc st.Joint_semantics.pc)) (fun st' ->
171      Monad.m_bind0 (Monad.max_def Errors.res0)
172        (Obj.magic
173          (Errors.opt_to_res (List.Cons ((Errors.MSG
174            ErrorMessages.FrameErrorOnPush), List.Nil))
175            st'.Joint_semantics.st_frms)) (fun frms ->
176        Monad.m_return0 (Monad.max_def Errors.res0)
177          (Joint_semantics.set_frms ERTL_semantics.eRTL_state
178            (Obj.magic (List.Cons ({ Types.fst =
179              (Obj.magic st'.Joint_semantics.regs).Types.fst; Types.snd =
180              st.Joint_semantics.pc.ByteValues.pc_block }, frms)))
181            (Joint_semantics.set_regs ERTL_semantics.eRTL_state
182              (Obj.magic { Types.fst =
183                (Identifiers.empty_map PreIdentifiers.RegisterTag);
184                Types.snd = (Obj.magic st'.Joint_semantics.regs).Types.snd })
185              st')))))
186
187(** val eval_ertlptr_seq :
188    AST.ident List.list -> 'a1 Joint_semantics.genv_gen ->
189    ERTLptr.ertlptr_seq -> AST.ident -> Joint_semantics.state ->
190    Joint_semantics.state Errors.res **)
191let eval_ertlptr_seq globals ge stm id st =
192  match stm with
193  | ERTLptr.Ertlptr_ertl seq ->
194    ERTL_semantics.eval_ertl_seq globals ge seq id st
195  | ERTLptr.LOW_ADDRESS (r, l) ->
196    Obj.magic
197      (Monad.m_bind0 (Monad.max_def Errors.res0)
198        (Obj.magic (Joint_semantics.gen_pc_from_label globals ge id l))
199        (fun pc_lab ->
200        let { Types.fst = addrl; Types.snd = addrh } =
201          ByteValues.beval_pair_of_pc pc_lab
202        in
203        Obj.magic (ERTL_semantics.ps_reg_store_status r addrl st)))
204  | ERTLptr.HIGH_ADDRESS (r, l) ->
205    Obj.magic
206      (Monad.m_bind0 (Monad.max_def Errors.res0)
207        (Obj.magic (Joint_semantics.gen_pc_from_label globals ge id l))
208        (fun pc_lab ->
209        let { Types.fst = addrl; Types.snd = addrh } =
210          ByteValues.beval_pair_of_pc pc_lab
211        in
212        Obj.magic (ERTL_semantics.ps_reg_store_status r addrh st)))
213
214(** val eRTLptr_sem_uns : 'a1 Joint_semantics.sem_unserialized_params **)
215let eRTLptr_sem_uns =
216  { Joint_semantics.st_pars = ERTL_semantics.eRTL_state;
217    Joint_semantics.acca_store_ = (Obj.magic ERTL_semantics.ps_reg_store);
218    Joint_semantics.acca_retrieve_ =
219    (Obj.magic ERTL_semantics.ps_reg_retrieve);
220    Joint_semantics.acca_arg_retrieve_ =
221    (Obj.magic ERTL_semantics.ps_arg_retrieve); Joint_semantics.accb_store_ =
222    (Obj.magic ERTL_semantics.ps_reg_store); Joint_semantics.accb_retrieve_ =
223    (Obj.magic ERTL_semantics.ps_reg_retrieve);
224    Joint_semantics.accb_arg_retrieve_ =
225    (Obj.magic ERTL_semantics.ps_arg_retrieve); Joint_semantics.dpl_store_ =
226    (Obj.magic ERTL_semantics.ps_reg_store); Joint_semantics.dpl_retrieve_ =
227    (Obj.magic ERTL_semantics.ps_reg_retrieve);
228    Joint_semantics.dpl_arg_retrieve_ =
229    (Obj.magic ERTL_semantics.ps_arg_retrieve); Joint_semantics.dph_store_ =
230    (Obj.magic ERTL_semantics.ps_reg_store); Joint_semantics.dph_retrieve_ =
231    (Obj.magic ERTL_semantics.ps_reg_retrieve);
232    Joint_semantics.dph_arg_retrieve_ =
233    (Obj.magic ERTL_semantics.ps_arg_retrieve);
234    Joint_semantics.snd_arg_retrieve_ =
235    (Obj.magic ERTL_semantics.ps_arg_retrieve);
236    Joint_semantics.pair_reg_move_ =
237    (Obj.magic ERTL_semantics.ertl_eval_move); Joint_semantics.save_frame =
238    (Obj.magic ertlptr_save_frame); Joint_semantics.setup_call =
239    (fun x x0 x1 st ->
240    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st));
241    Joint_semantics.fetch_external_args =
242    ERTL_semantics.ertl_fetch_external_args; Joint_semantics.set_result =
243    (Obj.magic ERTL_semantics.ertl_set_result);
244    Joint_semantics.call_args_for_main = (Obj.magic Nat.O);
245    Joint_semantics.call_dest_for_main = (Obj.magic Types.It);
246    Joint_semantics.read_result = (fun x x0 x1 st ->
247    Obj.magic
248      (Monad.m_return0 (Monad.max_def Errors.res0)
249        (List.map
250          (SemanticsUtils.hwreg_retrieve
251            (Obj.magic st.Joint_semantics.regs).Types.snd)
252          I8051.registerRets))); Joint_semantics.eval_ext_seq =
253    (fun gl ge stm id -> eval_ertlptr_seq gl ge (Obj.magic stm) id);
254    Joint_semantics.pop_frame = (fun x x0 x1 x2 ->
255    ERTL_semantics.ertl_pop_frame) }
256
257(** val eRTLptr_semantics : SemanticsUtils.sem_graph_params **)
258let eRTLptr_semantics =
259  { SemanticsUtils.sgp_pars =
260    (Joint.gp_to_p__o__stmt_pars__o__uns_pars ERTLptr.eRTLptr);
261    SemanticsUtils.sgp_sup = (fun _ -> eRTLptr_sem_uns);
262    SemanticsUtils.graph_pre_main_generator = ERTLptr.eRTLptr_premain }
263
Note: See TracBrowser for help on using the repository browser.