source: extracted/semantics_blocks.ml @ 2881

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

...

File size: 5.9 KB
Line 
1open Preamble
2
3open State
4
5open Bind_new
6
7open BindLists
8
9open String
10
11open Sets
12
13open Listb
14
15open LabelledObjects
16
17open BitVectorTrie
18
19open Graphs
20
21open I8051
22
23open Order
24
25open Registers
26
27open CostLabel
28
29open Hide
30
31open Proper
32
33open PositiveMap
34
35open Deqsets
36
37open ErrorMessages
38
39open PreIdentifiers
40
41open Errors
42
43open Extralib
44
45open Lists
46
47open Identifiers
48
49open Integers
50
51open AST
52
53open Division
54
55open Exp
56
57open Arithmetic
58
59open Setoids
60
61open Monad
62
63open Option
64
65open Extranat
66
67open Vector
68
69open Div_and_mod
70
71open Jmeq
72
73open Russell
74
75open List
76
77open Util
78
79open FoldStuff
80
81open BitVector
82
83open Types
84
85open Bool
86
87open Relations
88
89open Nat
90
91open Hints_declaration
92
93open Core_notation
94
95open Pts
96
97open Logic
98
99open Positive
100
101open Z
102
103open BitVectorZ
104
105open Pointers
106
107open ByteValues
108
109open BackEndOps
110
111open Joint
112
113open Blocks
114
115open StructuredTraces
116
117open ExtraGlobalenvs
118
119open I8051bis
120
121open BEMem
122
123open Events
124
125open IOMonad
126
127open IO
128
129open Extra_bool
130
131open Coqlib
132
133open Values
134
135open FrontEndVal
136
137open GenMem
138
139open FrontEndMem
140
141open Globalenvs
142
143open Joint_semantics
144
145open Traces
146
147open ExtraMonads
148
149open Deqsets_extra
150
151open TranslateUtils
152
153open SemanticsUtils
154
155(** val repeat_eval_seq_no_pc :
156    Traces.evaluation_params -> AST.ident -> Joint.joint_seq List.list ->
157    Joint_semantics.state -> __ **)
158let repeat_eval_seq_no_pc p curr_id =
159  Monad.m_fold (Monad.max_def Errors.res0)
160    (Obj.magic
161      (Joint_semantics.eval_seq_no_pc p.Traces.sparams p.Traces.globals
162        p.Traces.ev_genv curr_id))
163
164(** val produce_trace_any_any_free_aux :
165    Traces.prog_params -> Joint_semantics.state_pc -> AST.ident ->
166    Joint.joint_closed_internal_function -> Joint.joint_seq List.list -> __
167    List.list -> __ -> Joint_semantics.state ->
168    StructuredTraces.trace_any_any_free Types.sig0 **)
169let rec produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' =
170  (match b with
171   | List.Nil ->
172     (fun l0 dst0 st'0 _ _ _ -> StructuredTraces.Taaf_base (Obj.magic st))
173   | List.Cons (hd, tl) ->
174     (fun l0 ->
175       match l0 with
176       | List.Nil -> (fun dst0 st'0 _ _ -> assert false (* absurd case *))
177       | List.Cons (x, rest) ->
178         (fun dst0 ->
179           let mid =
180             match rest with
181             | List.Nil -> dst0
182             | List.Cons (mid, x0) -> mid
183           in
184           (fun st'0 _ _ _ ->
185           let mid_pc =
186             Joint_semantics.pc_of_point
187               (Traces.prog_params_to_ev_params__o__sparams p)
188               st.Joint_semantics.pc.ByteValues.pc_block mid
189           in
190           (match Joint_semantics.eval_seq_no_pc
191                    (Traces.make_global p).Traces.sparams
192                    (Traces.make_global p).Traces.globals
193                    (Traces.make_global p).Traces.ev_genv curr_id hd
194                    st.Joint_semantics.st_no_pc with
195            | Errors.OK st_mid ->
196              (fun _ ->
197                let tr_tl =
198                  produce_trace_any_any_free_aux p
199                    { Joint_semantics.st_no_pc = st_mid; Joint_semantics.pc =
200                    mid_pc; Joint_semantics.last_pop =
201                    st.Joint_semantics.last_pop } curr_id curr_fn tl rest
202                    dst0 st'0
203                in
204                StructuredTraces.taaf_cons (Traces.joint_abstract_status p)
205                  (Obj.magic st)
206                  (Obj.magic { Joint_semantics.st_no_pc = st_mid;
207                    Joint_semantics.pc = mid_pc; Joint_semantics.last_pop =
208                    st.Joint_semantics.last_pop })
209                  (Obj.magic { Joint_semantics.st_no_pc = st'0;
210                    Joint_semantics.pc =
211                    (Joint_semantics.pc_of_point
212                      (Traces.prog_params_to_ev_params__o__sparams p)
213                      { Joint_semantics.st_no_pc = st_mid;
214                      Joint_semantics.pc = mid_pc; Joint_semantics.last_pop =
215                      st.Joint_semantics.last_pop }.Joint_semantics.pc.ByteValues.pc_block
216                      dst0); Joint_semantics.last_pop =
217                    { Joint_semantics.st_no_pc = st_mid; Joint_semantics.pc =
218                    mid_pc; Joint_semantics.last_pop =
219                    st.Joint_semantics.last_pop }.Joint_semantics.last_pop })
220                  (Types.pi1 tr_tl))
221            | Errors.Error x0 -> (fun _ -> assert false (* absurd case *)))
222             __)))) l dst st' __ __ __
223
224(** val produce_trace_any_any_free :
225    Traces.prog_params -> Joint_semantics.state_pc -> AST.ident ->
226    Joint.joint_closed_internal_function -> Joint.joint_seq List.list -> __
227    List.list -> __ -> Joint_semantics.state ->
228    StructuredTraces.trace_any_any_free **)
229let produce_trace_any_any_free p st curr_id curr_fn b l dst st' =
230  Types.pi1 (produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st')
231
232(** val produce_trace_any_any_free_coerced :
233    Traces.prog_params -> Joint_semantics.state_pc -> AST.ident ->
234    Joint.joint_closed_internal_function -> Joint.joint_seq List.list -> __
235    List.list -> __ -> Joint_semantics.state ->
236    StructuredTraces.trace_any_any_free **)
237let produce_trace_any_any_free_coerced p st curr_id curr_fn b l dst st' =
238  List.list_inv_rect_Type0 b (fun _ _ _ ->
239    Obj.magic Errors.res_discr (Errors.OK st.Joint_semantics.st_no_pc)
240      (Errors.OK st') __ (fun _ ->
241      Logic.eq_rect_Type0 st.Joint_semantics.st_no_pc (fun _ ->
242        Logic.streicherK (Errors.OK st.Joint_semantics.st_no_pc)
243          (StructuredTraces.Taaf_step ((Obj.magic st), (Obj.magic st),
244          (Obj.magic { Joint_semantics.st_no_pc =
245            st.Joint_semantics.st_no_pc; Joint_semantics.pc =
246            (Joint_semantics.pc_of_point
247              (Traces.prog_params_to_ev_params__o__sparams p)
248              st.Joint_semantics.pc.ByteValues.pc_block dst);
249            Joint_semantics.last_pop = st.Joint_semantics.last_pop }),
250          (StructuredTraces.Taa_base (Obj.magic st))))) st' __))
251    (fun hd tl x _ ->
252    Logic.eq_rect_Type0 b (fun _ _ ->
253      produce_trace_any_any_free p st curr_id curr_fn b l dst st') (List.Cons
254      (hd, tl))) __ __
255
Note: See TracBrowser for help on using the repository browser.