source: driver/extracted/joint_fullexec.ml @ 3106

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

The initial status memory was not really initialized. Now it is.

File size: 3.2 KB
Line 
1open Preamble
2
3open StructuredTraces
4
5open ExtraMonads
6
7open Deqsets_extra
8
9open State
10
11open Bind_new
12
13open BindLists
14
15open Blocks
16
17open TranslateUtils
18
19open ExtraGlobalenvs
20
21open I8051bis
22
23open String
24
25open Sets
26
27open Listb
28
29open LabelledObjects
30
31open BitVectorTrie
32
33open Graphs
34
35open I8051
36
37open Order
38
39open Registers
40
41open BackEndOps
42
43open Joint
44
45open BEMem
46
47open CostLabel
48
49open Events
50
51open IOMonad
52
53open IO
54
55open Extra_bool
56
57open Coqlib
58
59open Values
60
61open FrontEndVal
62
63open Hide
64
65open ByteValues
66
67open Division
68
69open Z
70
71open BitVectorZ
72
73open Pointers
74
75open GenMem
76
77open FrontEndMem
78
79open Proper
80
81open PositiveMap
82
83open Deqsets
84
85open Extralib
86
87open Lists
88
89open Identifiers
90
91open Exp
92
93open Arithmetic
94
95open Vector
96
97open Div_and_mod
98
99open Util
100
101open FoldStuff
102
103open BitVector
104
105open Extranat
106
107open Integers
108
109open AST
110
111open ErrorMessages
112
113open Option
114
115open Setoids
116
117open Monad
118
119open Jmeq
120
121open Russell
122
123open Positive
124
125open PreIdentifiers
126
127open Bool
128
129open Relations
130
131open Nat
132
133open List
134
135open Hints_declaration
136
137open Core_notation
138
139open Pts
140
141open Logic
142
143open Types
144
145open Errors
146
147open Globalenvs
148
149open Joint_semantics
150
151open SemanticsUtils
152
153open Traces
154
155open Stacksize
156
157open SmallstepExec
158
159open Executions
160
161open Measurable
162
163(** val joint_exec :
164    Joint_semantics.sem_params -> (IO.io_out, IO.io_in)
165    SmallstepExec.trans_system **)
166let joint_exec g =
167  { SmallstepExec.is_final = (fun env ->
168    Obj.magic (Traces.joint_final g (Obj.magic env))); SmallstepExec.step =
169    (fun env st ->
170    Obj.magic
171      (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
172        (Obj.magic
173          (Joint_semantics.eval_state g (Obj.magic env).Traces.globals
174            (Obj.magic env).Traces.ev_genv (Obj.magic st))) (fun st' ->
175        let charge =
176          match Traces.joint_label_of_pc g (Obj.magic env)
177                  (Obj.magic st).Joint_semantics.pc with
178          | Types.None -> Events.e0
179          | Types.Some c -> Events.echarge c
180        in
181        Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = charge;
182          Types.snd = st' }))) }
183
184(** val joint_fullexec :
185    Joint_semantics.sem_params -> (IO.io_out, IO.io_in)
186    SmallstepExec.fullexec **)
187let joint_fullexec g =
188  { SmallstepExec.es1 = (joint_exec g); SmallstepExec.make_global =
189    (fun pr ->
190    Obj.magic
191      (Traces.joint_make_global { Traces.prog_spars = g; Traces.prog =
192        (Obj.magic pr).Types.fst; Traces.stack_sizes =
193        (Obj.magic pr).Types.snd })); SmallstepExec.make_initial_state =
194    (fun p_stacks ->
195    Obj.magic
196      (Traces.make_initial_state { Traces.prog_spars = g; Traces.prog =
197        (Obj.magic p_stacks).Types.fst; Traces.stack_sizes =
198        (Obj.magic p_stacks).Types.snd })) }
199
200(** val joint_preclassified_system :
201    Joint_semantics.sem_params -> Measurable.preclassified_system **)
202let joint_preclassified_system g =
203  { Measurable.pcs_exec = (joint_fullexec g); Measurable.pcs_labelled =
204    (fun env st ->
205    Bool.notb
206      (PositiveMap.is_none
207        (Traces.joint_label_of_pc g (Obj.magic env)
208          (Obj.magic st).Joint_semantics.pc))); Measurable.pcs_classify =
209    (fun env -> Obj.magic (Traces.joint_classify g (Obj.magic env)));
210    Measurable.pcs_callee = (fun env s _ ->
211    Traces.joint_call_ident g (Obj.magic env) (Obj.magic s)) }
212
Note: See TracBrowser for help on using the repository browser.