source: driver/extracted/eRTL_semantics.ml @ 3106

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 11.3 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
153type ertl_reg_env =
154  (ByteValues.beval Registers.register_env, SemanticsUtils.hw_register_env)
155  Types.prod
156
157(** val ps_reg_store :
158    PreIdentifiers.identifier -> ByteValues.beval -> ertl_reg_env ->
159    (ByteValues.beval Identifiers.identifier_map,
160    SemanticsUtils.hw_register_env) Types.prod Errors.res **)
161let ps_reg_store r v local_env =
162  let res = SemanticsUtils.reg_store r v local_env.Types.fst in
163  Errors.OK { Types.fst = res; Types.snd = local_env.Types.snd }
164
165(** val ps_reg_retrieve :
166    ertl_reg_env -> Registers.register -> ByteValues.beval Errors.res **)
167let ps_reg_retrieve local_env =
168  SemanticsUtils.reg_retrieve local_env.Types.fst
169
170(** val hw_reg_store :
171    I8051.register -> ByteValues.beval -> ertl_reg_env -> (ByteValues.beval
172    Registers.register_env, SemanticsUtils.hw_register_env) Types.prod
173    Errors.res **)
174let hw_reg_store r v local_env =
175  Errors.OK { Types.fst = local_env.Types.fst; Types.snd =
176    (SemanticsUtils.hwreg_store r v local_env.Types.snd) }
177
178(** val hw_reg_retrieve :
179    ertl_reg_env -> I8051.register -> ByteValues.beval Errors.res **)
180let hw_reg_retrieve local_env reg =
181  Errors.OK (SemanticsUtils.hwreg_retrieve local_env.Types.snd reg)
182
183(** val ps_arg_retrieve :
184    ertl_reg_env -> Registers.register Joint.argument -> ByteValues.beval
185    Errors.res **)
186let ps_arg_retrieve local_env = function
187| Joint.Reg r -> ps_reg_retrieve local_env r
188| Joint.Imm b ->
189  Obj.magic
190    (Monad.m_return0 (Monad.max_def Errors.res0) (ByteValues.BVByte b))
191
192(** val get_hwsp : ertl_reg_env -> ByteValues.xpointer Errors.res **)
193let get_hwsp st =
194  SemanticsUtils.hwreg_retrieve_sp st.Types.snd
195
196(** val set_hwsp : ertl_reg_env -> ByteValues.xpointer -> ertl_reg_env **)
197let set_hwsp st sp =
198  { Types.fst = st.Types.fst; Types.snd =
199    (SemanticsUtils.hwreg_store_sp st.Types.snd sp) }
200
201(** val eRTL_state : Joint_semantics.sem_state_params **)
202let eRTL_state =
203  { Joint_semantics.empty_framesT = (Obj.magic List.Nil);
204    Joint_semantics.empty_regsT = (fun sp ->
205    Obj.magic { Types.fst =
206      (Identifiers.empty_map PreIdentifiers.RegisterTag); Types.snd =
207      (SemanticsUtils.init_hw_register_env sp) }); Joint_semantics.load_sp =
208    (Obj.magic get_hwsp); Joint_semantics.save_sp = (Obj.magic set_hwsp) }
209
210(** val ertl_eval_move :
211    ertl_reg_env -> (ERTL.move_dst, ERTL.move_dst Joint.argument) Types.prod
212    -> __ **)
213let ertl_eval_move env pr =
214  Monad.m_bind0 (Monad.max_def Errors.res0)
215    (match pr.Types.snd with
216     | Joint.Reg src ->
217       (match src with
218        | ERTL.PSD r -> Obj.magic (ps_reg_retrieve env r)
219        | ERTL.HDW r -> Obj.magic (hw_reg_retrieve env r))
220     | Joint.Imm b ->
221       Monad.m_return0 (Monad.max_def Errors.res0) (ByteValues.BVByte b))
222    (fun v ->
223    match pr.Types.fst with
224    | ERTL.PSD r -> Obj.magic (ps_reg_store r v env)
225    | ERTL.HDW r -> Obj.magic (hw_reg_store r v env))
226
227(** val ertl_allocate_local :
228    PreIdentifiers.identifier -> ertl_reg_env -> (ByteValues.beval
229    Identifiers.identifier_map, SemanticsUtils.hw_register_env) Types.prod **)
230let ertl_allocate_local reg lenv =
231  { Types.fst =
232    (Identifiers.add PreIdentifiers.RegisterTag lenv.Types.fst reg
233      ByteValues.BVundef); Types.snd = lenv.Types.snd }
234
235(** val ertl_save_frame :
236    Joint_semantics.call_kind -> Types.unit0 -> Joint_semantics.state_pc ->
237    Joint_semantics.state Errors.res **)
238let ertl_save_frame x x0 st =
239  Obj.magic
240    (Monad.m_bind0 (Monad.max_def Errors.res0)
241      (Obj.magic
242        (Joint_semantics.push_ra eRTL_state st.Joint_semantics.st_no_pc
243          st.Joint_semantics.pc)) (fun st' ->
244      Monad.m_bind0 (Monad.max_def Errors.res0)
245        (Obj.magic
246          (Errors.opt_to_res (List.Cons ((Errors.MSG
247            ErrorMessages.FrameErrorOnPush), List.Nil))
248            st'.Joint_semantics.st_frms)) (fun frms ->
249        Monad.m_return0 (Monad.max_def Errors.res0)
250          (Joint_semantics.set_frms eRTL_state
251            (Obj.magic (List.Cons ({ Types.fst =
252              (Obj.magic st'.Joint_semantics.regs).Types.fst; Types.snd =
253              st.Joint_semantics.pc.ByteValues.pc_block }, frms)))
254            (Joint_semantics.set_regs eRTL_state
255              (Obj.magic { Types.fst =
256                (Identifiers.empty_map PreIdentifiers.RegisterTag);
257                Types.snd = (Obj.magic st'.Joint_semantics.regs).Types.snd })
258              st')))))
259
260(** val ertl_pop_frame :
261    Joint_semantics.state -> (Joint_semantics.state,
262    ByteValues.program_counter) Types.prod Errors.res **)
263let ertl_pop_frame st =
264  Obj.magic
265    (Monad.m_bind0 (Monad.max_def Errors.res0)
266      (Obj.magic
267        (Errors.opt_to_res (List.Cons ((Errors.MSG
268          ErrorMessages.FrameErrorOnPop), List.Nil))
269          st.Joint_semantics.st_frms)) (fun frms ->
270      match frms with
271      | List.Nil ->
272        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
273          ErrorMessages.FramesEmptyOnPop), List.Nil)))
274      | List.Cons (hd, tl) ->
275        let { Types.fst = local_mem; Types.snd = bl } = hd in
276        let st' =
277          Joint_semantics.set_regs eRTL_state
278            (Obj.magic { Types.fst = local_mem; Types.snd =
279              (Obj.magic st.Joint_semantics.regs).Types.snd })
280            (Joint_semantics.set_frms eRTL_state (Obj.magic tl) st)
281        in
282        Monad.m_bind2 (Monad.max_def Errors.res0)
283          (Obj.magic (Joint_semantics.pop_ra eRTL_state st')) (fun st'' pc ->
284          match Pointers.eq_block (Types.pi1 bl)
285                  (Types.pi1 pc.ByteValues.pc_block) with
286          | Bool.True ->
287            Obj.magic (Errors.OK { Types.fst = st''; Types.snd = pc })
288          | Bool.False ->
289            Obj.magic (Errors.Error (List.Cons ((Errors.MSG
290              ErrorMessages.BlockInFramesCorrupted), List.Nil))))))
291
292(** val ertl_fetch_external_args :
293    AST.external_function -> Joint_semantics.state -> __ -> Values.val0
294    List.list Errors.res **)
295let ertl_fetch_external_args _ =
296  failwith "AXIOM TO BE REALIZED"
297
298(** val ertl_set_result :
299    Values.val0 List.list -> Types.unit0 -> Joint_semantics.state ->
300    Joint_semantics.state Errors.res **)
301let ertl_set_result _ =
302  failwith "AXIOM TO BE REALIZED"
303
304(** val ps_reg_store_status :
305    Registers.register -> ByteValues.beval -> Joint_semantics.state ->
306    Joint_semantics.state Errors.res **)
307let ps_reg_store_status dst v st =
308  let env = st.Joint_semantics.regs in
309  Obj.magic
310    (Monad.m_bind0 (Monad.max_def Errors.res0)
311      (Obj.magic (ps_reg_store dst v (Obj.magic env))) (fun env' ->
312      Monad.m_return0 (Monad.max_def Errors.res0)
313        (Joint_semantics.set_regs eRTL_state env' st)))
314
315(** val eval_ertl_seq :
316    AST.ident List.list -> 'a1 Joint_semantics.genv_gen -> ERTL.ertl_seq ->
317    AST.ident -> Joint_semantics.state -> Joint_semantics.state Errors.res **)
318let eval_ertl_seq globals ge stm id st =
319  Obj.magic
320    (Monad.m_bind0 (Monad.max_def Errors.res0)
321      (Obj.magic
322        (Errors.opt_to_res (Errors.msg ErrorMessages.FunctionNotFound)
323          (ge.Joint_semantics.stack_sizes id))) (fun framesize ->
324      let framesize0 =
325        Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
326          (Nat.S (Nat.S Nat.O)))))))) framesize
327      in
328      (match stm with
329       | ERTL.Ertl_new_frame ->
330         Monad.m_bind0 (Monad.max_def Errors.res0)
331           (Obj.magic (Joint_semantics.sp eRTL_state st)) (fun sp ->
332           let newsp =
333             Pointers.neg_shift_pointer (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
334               (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Types.pi1 sp) framesize0
335           in
336           Monad.m_return0 (Monad.max_def Errors.res0)
337             (Joint_semantics.set_sp eRTL_state newsp st))
338       | ERTL.Ertl_del_frame ->
339         Monad.m_bind0 (Monad.max_def Errors.res0)
340           (Obj.magic (Joint_semantics.sp eRTL_state st)) (fun sp ->
341           let newsp =
342             Pointers.shift_pointer (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
343               (Nat.S (Nat.S Nat.O)))))))) (Types.pi1 sp) framesize0
344           in
345           Monad.m_return0 (Monad.max_def Errors.res0)
346             (Joint_semantics.set_sp eRTL_state newsp st))
347       | ERTL.Ertl_frame_size dst ->
348         Obj.magic
349           (ps_reg_store_status dst (ByteValues.BVByte framesize0) st))))
350
351(** val eRTL_sem_uns : 'a1 Joint_semantics.sem_unserialized_params **)
352let eRTL_sem_uns =
353  { Joint_semantics.st_pars = eRTL_state; Joint_semantics.acca_store_ =
354    (Obj.magic ps_reg_store); Joint_semantics.acca_retrieve_ =
355    (Obj.magic ps_reg_retrieve); Joint_semantics.acca_arg_retrieve_ =
356    (Obj.magic ps_arg_retrieve); Joint_semantics.accb_store_ =
357    (Obj.magic ps_reg_store); Joint_semantics.accb_retrieve_ =
358    (Obj.magic ps_reg_retrieve); Joint_semantics.accb_arg_retrieve_ =
359    (Obj.magic ps_arg_retrieve); Joint_semantics.dpl_store_ =
360    (Obj.magic ps_reg_store); Joint_semantics.dpl_retrieve_ =
361    (Obj.magic ps_reg_retrieve); Joint_semantics.dpl_arg_retrieve_ =
362    (Obj.magic ps_arg_retrieve); Joint_semantics.dph_store_ =
363    (Obj.magic ps_reg_store); Joint_semantics.dph_retrieve_ =
364    (Obj.magic ps_reg_retrieve); Joint_semantics.dph_arg_retrieve_ =
365    (Obj.magic ps_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
366    (Obj.magic ps_arg_retrieve); Joint_semantics.pair_reg_move_ =
367    (Obj.magic ertl_eval_move); Joint_semantics.save_frame =
368    (Obj.magic ertl_save_frame); Joint_semantics.setup_call =
369    (fun x x0 x1 st ->
370    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st));
371    Joint_semantics.fetch_external_args = ertl_fetch_external_args;
372    Joint_semantics.set_result = (Obj.magic ertl_set_result);
373    Joint_semantics.call_args_for_main = (Obj.magic Nat.O);
374    Joint_semantics.call_dest_for_main = (Obj.magic Types.It);
375    Joint_semantics.read_result = (fun x x0 x1 st ->
376    Obj.magic
377      (Monad.m_return0 (Monad.max_def Errors.res0)
378        (List.map
379          (SemanticsUtils.hwreg_retrieve
380            (Obj.magic st.Joint_semantics.regs).Types.snd)
381          I8051.registerRets))); Joint_semantics.eval_ext_seq =
382    (fun gl ge stm id -> eval_ertl_seq gl ge (Obj.magic stm) id);
383    Joint_semantics.pop_frame = (fun x x0 x1 x2 -> ertl_pop_frame) }
384
385(** val eRTL_semantics : SemanticsUtils.sem_graph_params **)
386let eRTL_semantics =
387  { SemanticsUtils.sgp_pars =
388    (Joint.gp_to_p__o__stmt_pars__o__uns_pars ERTL.eRTL);
389    SemanticsUtils.sgp_sup = (fun _ -> eRTL_sem_uns);
390    SemanticsUtils.graph_pre_main_generator = ERTL.eRTL_premain }
391
Note: See TracBrowser for help on using the repository browser.