Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
verimag
synchrone
lutin
Commits
bf5cb12d
Commit
bf5cb12d
authored
Feb 10, 2016
by
Erwan Jahier
Browse files
Add a exception contunuation to handle Lutin Exceptions correctly in rdbg.
parent
35dea30a
Changes
6
Hide whitespace changes
Inline
Side-by-side
examples/lutin/crazy-rabbit/Makefile
View file @
bf5cb12d
...
...
@@ -23,7 +23,7 @@ clean:
test.rif
:
$(EXPDIR) rabbit.cmxs
rm
-f
test.rif0 .lurette_rc
$(LURETTETOP)
-go
--output
test.rif0
-seed
3
3
\
$(LURETTETOP)
-go
--output
test.rif0
-seed
3
4
\
-
rp
"sut:ocaml:rabbit.cmxs:"
\
-
rp
'env:lutin:rabbit.lut:-main:rabbit:-L:libm.so:-loc'
&&
\
grep
-v
"lurette chronogram"
test.rif0 |
\
...
...
lutin/src/lutExe.ml
View file @
bf5cb12d
...
...
@@ -699,7 +699,7 @@ type continuation = {
}
type
continuation_ldbg
=
{
doit_ldbg
:
Event
.
ctx
->
behavior
->
(
Event
.
ctx
->
behavior
->
Event
.
t
)
->
(
Event
.
ctx
->
Event
.
t
)
->
Event
.
t
;
->
(
Event
.
ctx
->
Event
.
t
)
->
(
Event
.
ctx
->
string
->
Event
.
t
)
->
Event
.
t
;
dbg_ldbg
:
cont_mnemo
list
}
...
...
@@ -711,7 +711,7 @@ let (mk_cont : (behavior -> behavior) -> cont_mnemo -> continuation -> continuat
let
(
mk_cont_ldbg
:
Event
.
ctx
->
(
Event
.
ctx
->
behavior
->
(
Event
.
ctx
->
behavior
->
Event
.
t
)
->
(
Event
.
ctx
->
Event
.
t
)
->
Event
.
t
)
->
(
Event
.
ctx
->
Event
.
t
)
->
(
Event
.
ctx
->
string
->
Event
.
t
)
->
Event
.
t
)
->
cont_mnemo
->
continuation_ldbg
->
(
Event
.
ctx
->
continuation_ldbg
->
Event
.
t
)
->
Event
.
t
)
=
fun
ctx
f
d
cin
cont
->
...
...
@@ -1434,8 +1434,9 @@ let rec (genpath_ldbg :
Event
.
ctx
->
(
Event
.
ctx
->
behavior
->
Event
.
t
)
->
(
Event
.
ctx
->
Event
.
t
)
->
(
Event
.
ctx
->
string
->
Event
.
t
)
->
Event
.
t
)
=
fun
it
data
x
ctx
cont
fail_cont
->
(* data env = inputs + pres *)
(
fun
it
data
x
ctx
cont
fail_cont
excn_cont
->
(* data env = inputs + pres *)
(
(*-------------------------------------------*)
(* Correspondance id de trace -> trace exp
N.B. on traque les récursions ? *)
...
...
@@ -1450,9 +1451,10 @@ let rec (genpath_ldbg :
let
rec
(
rec_genpath_ldbg
:
Event
.
ctx
->
branch_ldbg
->
(
Event
.
ctx
->
behavior
->
Event
.
t
)
->
(
Event
.
ctx
->
Event
.
t
)
->
(
Event
.
ctx
->
string
->
Event
.
t
)
->
Event
.
t
)
=
fun
ctx
br
cont
fail_cont
->
(
fun
ctx
br
cont
fail_cont
excn_cont
->
(
let
data
=
br
.
br_data_ldbg
in
let
x
=
br
.
br_ctrl_ldbg
in
let
acc
=
br
.
br_acc_ldbg
in
...
...
@@ -1472,18 +1474,20 @@ let rec (genpath_ldbg :
match
br
.
br_ctrl_ldbg
with
(** Aliased trace *)
|
TE_ref
s
->
(
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
id2trace
s
})
cont
fail_cont
)
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
id2trace
s
})
cont
fail_cont
excn_cont
)
(** Leaves: apply cont *)
|
TE_raise
s
->
br_cont
.
doit_ldbg
ctx
(
Raise
s
)
cont
fail_cont
|
TE_eps
->
br_cont
.
doit_ldbg
ctx
Vanish
cont
fail_cont
|
TE_raise
s
->
br_cont
.
doit_ldbg
ctx
(
Raise
s
)
cont
fail_cont
excn_cont
|
TE_eps
->
br_cont
.
doit_ldbg
ctx
Vanish
cont
fail_cont
excn_cont
|
TE_noeps
e
->
(
(** No eps: forbids e to vanish (but not to raise !) *)
let
cont2
ctx
noeps_cont
=
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e
;
br_cont_ldbg
=
noeps_cont
})
cont
fail_cont
ctx
({
br
with
br_ctrl_ldbg
=
e
;
br_cont_ldbg
=
noeps_cont
})
cont
fail_cont
excn_cont
in
mk_cont_ldbg
ctx
(
fun
ctx
a
lcont
fail_cont
->
(
fun
ctx
a
lcont
fail_cont
excn_cont
->
Verbose
.
exe
~
flag
:
dbg
(
fun
()
->
Printf
.
printf
...
...
@@ -1491,7 +1495,7 @@ let rec (genpath_ldbg :
(
string_of_behavior
a
)
(
string_of_control_state
x
));
match
a
with
|
Vanish
->
fail_cont
ctx
|
z
->
br_cont
.
doit_ldbg
ctx
z
lcont
fail_cont
|
z
->
br_cont
.
doit_ldbg
ctx
z
lcont
fail_cont
excn_cont
)
(
Cnoeps
)
br_cont
...
...
@@ -1515,7 +1519,8 @@ let rec (genpath_ldbg :
Event
.
nb
=
enb
;
Event
.
lang
=
"lutin"
;
Event
.
next
=
(
fun
()
->
(
br_cont
.
doit_ldbg
ctx
(
Goto
(
new_acc
,
TE_eps
))
cont
fail_cont
));
(
br_cont
.
doit_ldbg
ctx
(
Goto
(
new_acc
,
TE_eps
))
cont
fail_cont
excn_cont
));
Event
.
sinfo
=
Some
(
fun
()
->
{
Event
.
expr
=
cstr
;
Event
.
more
=
None
;
...
...
@@ -1592,10 +1597,10 @@ let rec (genpath_ldbg :
let
(
cont2
:
Event
.
ctx
->
continuation_ldbg
->
Event
.
t
)
=
fun
ctx
fby_cont
->
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
te1
;
br_cont_ldbg
=
fby_cont
})
cont
fail_cont
br_cont_ldbg
=
fby_cont
})
cont
fail_cont
excn_cont
in
mk_cont_ldbg
ctx
(
fun
ctx
a
lcont
fail_cont
->
(
fun
ctx
a
lcont
fail_cont
excn_cont
->
Verbose
.
exe
~
flag
:
dbg
(
fun
()
->
Printf
.
printf
"-- fby_cont (%s)
\n
in context %s
\n
"
...
...
@@ -1603,10 +1608,11 @@ let rec (genpath_ldbg :
(
string_of_control_state
x
));
match
a
with
|
Goto
(
cl
,
n
)
->
br_cont
.
doit_ldbg
ctx
(
Goto
(
cl
,
put_in_seq
n
te2
))
lcont
fail_cont
br_cont
.
doit_ldbg
ctx
(
Goto
(
cl
,
put_in_seq
n
te2
))
lcont
fail_cont
excn_cont
|
Vanish
->
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
te2
})
lcont
fail_cont
|
Raise
_
->
br_cont
.
doit_ldbg
ctx
a
lcont
fail_cont
lcont
fail_cont
excn_cont
|
Raise
_
->
br_cont
.
doit_ldbg
ctx
a
lcont
fail_cont
excn_cont
)
(
Cfby
te2
)
br_cont
...
...
@@ -1616,9 +1622,10 @@ let rec (genpath_ldbg :
|
TE_prio
(
te
::
tel
)
->
(
(** Priority: Deadlock is catched HERE *)
let
fail_cont
ctx
=
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
(
TE_prio
tel
)})
cont
fail_cont
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
(
TE_prio
tel
)})
cont
fail_cont
excn_cont
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
te
})
cont
fail_cont
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
te
})
cont
fail_cont
excn_cont
)
(** Try similar to a recurse priority *)
|
TE_try
(
e
,
eco
)
->
(
...
...
@@ -1627,22 +1634,24 @@ let rec (genpath_ldbg :
|
Some
e'
->
e'
|
None
->
TE_eps
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
ec
})
cont
fail_cont
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
ec
})
cont
fail_cont
excn_cont
in
let
cont2
ctx
try_cont
=
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e
;
br_cont_ldbg
=
try_cont
})
cont
fail_cont
({
br
with
br_ctrl_ldbg
=
e
;
br_cont_ldbg
=
try_cont
})
cont
fail_cont
excn_cont
in
mk_cont_ldbg
ctx
(
fun
ctx
a
lcont
fail_cont
->
(
fun
ctx
a
lcont
fail_cont
excn_cont
->
Verbose
.
exe
~
flag
:
dbg
(
fun
()
->
Printf
.
printf
"-- try_cont (%s)
\n
in context %s
\n
"
(
string_of_behavior
a
)
(
string_of_control_state
x
));
match
a
with
|
Goto
(
cl
,
n
)
->
br_cont
.
doit_ldbg
ctx
(
Goto
(
cl
,
TE_try
(
n
,
eco
)))
lcont
fail_cont
|
_
->
br_cont
.
doit_ldbg
ctx
a
lcont
fail_cont
br_cont
.
doit_ldbg
ctx
(
Goto
(
cl
,
TE_try
(
n
,
eco
)))
lcont
fail_cont
excn_cont
|
_
->
br_cont
.
doit_ldbg
ctx
a
lcont
fail_cont
excn_cont
)
(
Ctry
eco
)
br_cont
...
...
@@ -1657,14 +1666,14 @@ let rec (genpath_ldbg :
TE_eps
]
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
excn_cont
)
(** INFINITE STRONG LOOP *)
(* must behaves exactly as: (te\eps fby omega te) *)
|
TE_omega
te
->
(
let
e'
=
put_in_seq
(
TE_noeps
te
)
(
TE_omega
te
)
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
excn_cont
)
(** ASSERT *)
(* default assert is WEAK for backward compatibility
...
...
@@ -1681,7 +1690,7 @@ let rec (genpath_ldbg :
,
None
)
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
excn_cont
)
(** STRONG ASSERT *)
(* must behave EXACTLY as
...
...
@@ -1697,7 +1706,7 @@ let rec (genpath_ldbg :
,
None
)
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
excn_cont
)
(** Exist: problem modifies the data and support, and the cont *)
|
TE_exist
(
ectx
,
te
)
->
(
...
...
@@ -1718,20 +1727,20 @@ let rec (genpath_ldbg :
let
new_pres
=
List
.
fold_left
addp
data
.
pres
ectx
in
let
new_data
=
{
data
with
pres
=
new_pres
}
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
te
;
br_data_ldbg
=
new_data
})
cont
fail_cont
cont
fail_cont
excn_cont
)
(** Parallel: at least one ? *)
|
TE_para
([])
->
assert
false
|
TE_para
([
e
])
->
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e
})
cont
fail_cont
cont
fail_cont
excn_cont
|
TE_para
(
e
::
el
)
->
(
(* continuation for the head statement *)
let
cont2
ctx
para_head_cont
=
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e
;
br_cont_ldbg
=
para_head_cont
})
cont
fail_cont
br_cont_ldbg
=
para_head_cont
})
cont
fail_cont
excn_cont
in
mk_cont_ldbg
ctx
(
fun
ctx
a
lcont
fail_cont
->
(
fun
ctx
a
lcont
fail_cont
excn_cont
->
Verbose
.
exe
~
flag
:
dbg
(
fun
()
->
...
...
@@ -1739,11 +1748,11 @@ let rec (genpath_ldbg :
(
string_of_behavior
a
)
(
string_of_control_state
x
));
match
a
with
(* 1st raises s: whole raises s *)
|
Raise
s
->
br_cont
.
doit_ldbg
ctx
(
Raise
s
)
lcont
fail_cont
|
Raise
s
->
br_cont
.
doit_ldbg
ctx
(
Raise
s
)
lcont
fail_cont
excn_cont
(* 1st vanishes: others continue *)
|
Vanish
->
(
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
TE_para
(
el
)})
lcont
fail_cont
lcont
fail_cont
excn_cont
)
(* 1st do a trans ... *)
|
Goto
(
cl
,
n
)
->
(
...
...
@@ -1757,20 +1766,21 @@ let rec (genpath_ldbg :
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
TE_para
(
el
);
br_acc_ldbg
=
tail_acc
;
br_cont_ldbg
=
para_tail_cont
})
lcont
fail_cont
br_cont_ldbg
=
para_tail_cont
})
lcont
fail_cont
excn_cont
in
mk_cont_ldbg
ctx
(
fun
ctx
a
lcont
fail_cont
->
(
fun
ctx
a
lcont
fail_cont
excn_cont
->
match
a
with
(* others vanish, 1st continue *)
|
Vanish
->
br_cont
.
doit_ldbg
ctx
(
Goto
(
cl
,
n
))
lcont
fail_cont
ctx
(
Goto
(
cl
,
n
))
lcont
fail_cont
excn_cont
(* others raise -> forbidden *)
|
Raise
s
->
fail_cont
ctx
|
Goto
(
tcl
,
tn
)
->
(
(* N.B. cl IS ALREADY accumulated in tcl *)
br_cont
.
doit_ldbg
ctx
(
Goto
(
tcl
,
put_in_para
n
tn
))
lcont
fail_cont
ctx
(
Goto
(
tcl
,
put_in_para
n
tn
))
lcont
fail_cont
excn_cont
)
)
(
Cpara_tail
(
cl
,
n
))
...
...
@@ -1786,10 +1796,10 @@ let rec (genpath_ldbg :
|
TE_catch
(
i
,
e
,
eco
)
->
(
let
cont2
ctx
catch_cont
=
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e
;
br_cont_ldbg
=
catch_cont
})
cont
fail_cont
br_cont_ldbg
=
catch_cont
})
cont
fail_cont
excn_cont
in
mk_cont_ldbg
ctx
(
fun
ctx
a
lcont
fail_cont
->
(
fun
ctx
a
lcont
fail_cont
excn_cont
->
Verbose
.
exe
~
flag
:
dbg
(
fun
()
->
...
...
@@ -1798,17 +1808,17 @@ let rec (genpath_ldbg :
match
a
with
|
Goto
(
cl
,
n
)
->
br_cont
.
doit_ldbg
ctx
(
Goto
(
cl
,
TE_catch
(
i
,
n
,
eco
)))
lcont
fail_cont
lcont
fail_cont
excn_cont
|
Raise
x
->
(
if
(
x
==
i
)
then
(
match
eco
with
|
None
->
br_cont
.
doit_ldbg
ctx
Vanish
lcont
fail_cont
|
None
->
br_cont
.
doit_ldbg
ctx
Vanish
lcont
fail_cont
excn_cont
|
Some
ec
->
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
ec
})
lcont
fail_cont
)
else
br_cont
.
doit_ldbg
ctx
(
Raise
x
)
lcont
fail_cont
lcont
fail_cont
excn_cont
)
else
br_cont
.
doit_ldbg
ctx
(
Raise
x
)
lcont
fail_cont
excn_cont
)
|
_
->
br_cont
.
doit_ldbg
ctx
a
lcont
fail_cont
|
_
->
br_cont
.
doit_ldbg
ctx
a
lcont
fail_cont
excn_cont
)
(
Ccatch
(
i
,
eco
))
br_cont
...
...
@@ -1837,7 +1847,7 @@ let rec (genpath_ldbg :
|
[]
->
raise
LocalDeadlock
|
[(
_
,
e
)]
->
e
|
_
->
TE_dyn_choice
(
sum
,
cel
)
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
excn_cont
with
LocalDeadlock
->
fail_cont
ctx
)
(* ad hoc node for dynamic simulation:
...
...
@@ -1865,7 +1875,7 @@ let rec (genpath_ldbg :
|
(
wc
,
e
)
::
cel'
->
TE_prio
[
e
;
TE_dyn_choice
(
sum
-
wc
,
cel'
)
]
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
excn_cont
)
(** Probabilistic loops
just like for choice, we use an ad hoc internal structure
...
...
@@ -1893,7 +1903,7 @@ let rec (genpath_ldbg :
|
_
->
TE_dyn_choice
(
gw
+
sw
,
[
(
gw
,
goon_branch
);(
sw
,
TE_eps
)])
)
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
excn_cont
with
LocalDeadlock
->
fail_cont
ctx
)
(** N.B. the "cpt" here is a unique identifier used for compilation
...
...
@@ -1906,7 +1916,7 @@ let rec (genpath_ldbg :
if
((
imin
>=
0
)
&&
(
imin
<=
imax
))
then
(
(* HERE *)
let
e'
=
TE_dyn_loop
(
LoopWeights
.
interval
imin
imax
,
0
,
te
)
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
excn_cont
)
else
(
(* HERE: need to have a real notion of run-time error with source ref *)
let
msg
=
Printf
.
sprintf
...
...
@@ -1925,7 +1935,7 @@ let rec (genpath_ldbg :
if
((
iec
>
0
)
&&
(
iav
>
iec
)
&&
(
iec
<=
((
20
*
iav
)
/
100
)))
then
(
(* HERE *)
let
e'
=
TE_dyn_loop
(
LoopWeights
.
average
iav
iec
,
0
,
te
)
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
})
cont
fail_cont
excn_cont
)
else
(
(* HERE: need to have a real notion of run-time error with source ref *)
let
msg
=
Printf
.
sprintf
...
...
@@ -1968,16 +1978,16 @@ let rec (genpath_ldbg :
let
zeexe
=
of_expanded_code
it
.
arg_opt
zecode
in
let
inits
=
get_init_internal_state
zeexe
in
let
(
cont2
:
Event
.
ctx
->
Reactive
.
prg_ldbg
->
(
Event
.
ctx
->
Event
.
t
)
->
Event
.
t
)
=
fun
ctx
zereact
fail_cont
->
->
(
Event
.
ctx
->
string
->
Event
.
t
)
->
Event
.
t
)
=
fun
ctx
zereact
fail_cont
excn_cont
->
let
outids
=
List
.
map
(
fun
(
id
,_
)
->
id
)
vars
in
(* build the initial TE_dyn_erun *)
let
e'
=
TE_dyn_erun_ldbg
(
rid
,
zereact
,
outids
,
args
,
e
)
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
;
br_data_ldbg
=
new_data
})
cont
fail_cont
br_data_ldbg
=
new_data
})
cont
fail_cont
excn_cont
in
cont2
ctx
(
Reactive
.
DoStep_ldbg
(
to_reactive_prg_ldbg
rid
zeexe
inits
))
fail_cont
fail_cont
excn_cont
(* builds the corresponding abstract reactive prg *)
)
...
...
@@ -1985,9 +1995,23 @@ let rec (genpath_ldbg :
|
TE_dyn_erun_ldbg
(
rid
,
react
,
vars
,
args
,
e
)
->
(
(* Evaluates args in context *)
let
eval_arg
x
=
compute_exp
it
data
x
in
let
fail_cont
ctx
=
let
msg
=
Printf
.
sprintf
"Run-time error: unexpected END while running
\"
%s
\"
"
rid
in
raise
(
Global_error
msg
)
in
let
excn_cont
ctx
x
=
let
msg
=
Printf
.
sprintf
"Run-time error: unexpected EXCEPTION
\"
%s
\"
when running
\"
%s
\"
"
x
rid
in
raise
(
Global_error
msg
)
in
let
ins
=
List
.
map
eval_arg
args
in
(* call the reactive prog *)
try
(
let
(
cont3
:
Event
.
ctx
->
Reactive
.
prg_ldbg
->
Value
.
t
list
->
Event
.
t
)
=
fun
ctx
react'
outs
->
(* stores the values in the LocalIns vars *)
...
...
@@ -2009,10 +2033,10 @@ let rec (genpath_ldbg :
({
br
with
br_ctrl_ldbg
=
e
;
br_data_ldbg
=
new_data
;
br_cont_ldbg
=
run_cont
})
cont
fail_cont
br_cont_ldbg
=
run_cont
})
cont
fail_cont
excn_cont
in
mk_cont_ldbg
ctx
(
fun
ctx
a
lcont
fail_cont
->
(
fun
ctx
a
lcont
fail_cont
excn_cont
->
Verbose
.
exe
~
flag
:
dbgrun
(
fun
()
->
...
...
@@ -2022,8 +2046,8 @@ let rec (genpath_ldbg :
|
Goto
(
cl
,
n
)
->
br_cont
.
doit_ldbg
ctx
(
Goto
(
cl
,
TE_dyn_erun_ldbg
(
rid
,
react'
,
vars
,
args
,
n
)))
lcont
fail_cont
|
_
->
br_cont
.
doit_ldbg
ctx
a
lcont
fail_cont
lcont
fail_cont
excn_cont
|
_
->
br_cont
.
doit_ldbg
ctx
a
lcont
fail_cont
excn_cont
)
(
Crun
(
rid
))
br_cont
...
...
@@ -2045,25 +2069,11 @@ let rec (genpath_ldbg :
Event
.
data
=
ctx
.
Event
.
ctx_data
;
Event
.
sinfo
=
None
;
Event
.
next
=
(
fun
()
->
Reactive
.
step_ldbg
ctx
react
ins
cont3
fail_cont
);
(
fun
()
->
Reactive
.
step_ldbg
ctx
react
ins
cont3
fail_cont
excn_cont
);
Event
.
terminate
=
ctx
.
Event
.
ctx_terminate
;
}
in
event
)
with
(* HERE: semantics, decide what to do if run stops ??? *)
|
Stop
->
let
msg
=
Printf
.
sprintf
"Run-time error: unexpected END while running
\"
%s
\"
"
rid
in
raise
(
Global_error
msg
)
|
Exception
x
->
let
msg
=
Printf
.
sprintf
"Run-time error: unexpected EXCEPTION
\"
%s
\"
when running
\"
%s
\"
"
x
rid
in
raise
(
Global_error
msg
)
)
(* run
andexp is the post-constraint /\(glob = loc)
...
...
@@ -2108,7 +2118,7 @@ let rec (genpath_ldbg :
fun
ctx
zereact
->
let
e'
=
TE_dyn_run_ldbg
(
rid
,
zereact
,
andexp
,
vars
,
args
,
e
,
si
)
in
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e'
;
br_data_ldbg
=
new_data
})
cont
fail_cont
br_data_ldbg
=
new_data
})
cont
fail_cont
excn_cont
in
cont2
ctx
(
Reactive
.
DoStep_ldbg
(
to_reactive_prg_ldbg
rid
zeexe
inits
))
)
...
...
@@ -2123,7 +2133,16 @@ let rec (genpath_ldbg :
let
eval_arg
x
=
compute_exp
it
data
x
in
let
ins
=
List
.
map
eval_arg
args
in
(* call the reactive prog *)
try
(
let
fail_cont
ctx
=
(* Emulate the "raise Stop" using the failure continuation.
Should'nt i need a stop continuation instead ? Are Stop and
Deadlock really different ?
*)
br_cont
.
doit_ldbg
ctx
Vanish
cont
fail_cont
excn_cont
in
let
excn_cont
ctx
x
=
br_cont
.
doit_ldbg
ctx
(
Raise
x
)
cont
fail_cont
excn_cont
in
let
(
cont3
:
Event
.
ctx
->
Reactive
.
prg_ldbg
->
Value
.
t
list
->
Event
.
t
)
=
fun
ctx
react'
outs
->
(* outs : Value.t list *)
...
...
@@ -2171,10 +2190,10 @@ let rec (genpath_ldbg :
(* recursively execute e in this new data env *)
rec_genpath_ldbg
ctx
({
br
with
br_ctrl_ldbg
=
e
;
br_data_ldbg
=
new_data
;
br_cont_ldbg
=
run_cont
})
cont
fail_cont
br_cont_ldbg
=
run_cont
})
cont
fail_cont
excn_cont
in
mk_cont_ldbg
ctx
(
fun
ctx
a
cont
fail_cont
->
(
fun
ctx
a
cont
fail_cont
excn_cont
->
Verbose
.
exe
~
flag
:
dbgrun
(
fun
()
->
...
...
@@ -2187,28 +2206,21 @@ let rec (genpath_ldbg :
br_cont
.
doit_ldbg
ctx
(
Goto
(
cl'
,
TE_dyn_run_ldbg
(
rid
,
react'
,
andexp
,
vars
,
args
,
n
,
si
)))
cont
fail_cont
cont
fail_cont
excn_cont
)
|
_
->
br_cont
.
doit_ldbg
ctx
a
cont
fail_cont
|
_
->
br_cont
.
doit_ldbg
ctx
a
cont
fail_cont
excn_cont
)
(
Crun
(
rid
))
br_cont
cont2
in
Reactive
.
step_ldbg
ctx
react
ins
cont3
fail_cont
)
with
(* HERE: semantics, decide what to do if run stops ??? *)
(* Stop <=> Vanish *)
|
Stop
->
br_cont
.
doit_ldbg
ctx
Vanish
cont
fail_cont
(* Exception <=> Raise *)
|
Exception
x
->
br_cont
.
doit_ldbg
ctx
(
Raise
x
)
cont
fail_cont
(* Deadlock <=? Deadlock *)
Reactive
.
step_ldbg
ctx
react
ins
cont3
fail_cont
excn_cont
)
)
(* gen_path_rec *)
in
(* Top-level branch *)
let
top_cont
:
continuation_ldbg
=
{
doit_ldbg
=
(
fun
ctx
a
cont
fail_cont
->
cont
ctx
a
);
dbg_ldbg
=
[]
}
{
doit_ldbg
=
(
fun
ctx
a
cont
fail_cont
excn_cont
->
cont
ctx
a
);
dbg_ldbg
=
[]
}
in
let
init_branch
=
{
br_ctrl_ldbg
=
x
;
...
...
@@ -2232,7 +2244,7 @@ rec_genpath_ldbg ctx init_branch
);
cont
ctx
b
)
fail_cont
fail_cont
excn_cont
)
(* end of genpath_ldbg ? *)
(* performs a reactive step in a way compatible with the interface Reactive, i.e.
...
...
@@ -2242,8 +2254,8 @@ rec_genpath_ldbg ctx init_branch
and
(
to_reactive_prg_ldbg
:
string
->
t
->
internal_state
->
Event
.
ctx
->
Value
.
t
list
->
(
Event
.
ctx
->
Reactive
.
prg_ldbg
->
Value
.
t
list
->
Event
.
t
)
->
(
Event
.
ctx
->
Event
.
t
)
->
Event
.
t
)
=
fun
rid
it
curstate
ctx
invals
cont
fail_cont
->
(
Event
.
ctx
->
Event
.
t
)
->
(
Event
.
ctx
->
string
->
Event
.
t
)
->
Event
.
t
)
=
fun
rid
it
curstate
ctx
invals
cont
fail_cont
excn_cont
->
let
rid_ctx
=
ctx
.
Event
.
ctx_name
in
let
d_ctx
=
ctx
.
Event
.
ctx_depth
in
let
(
cstate
,
pres
)
=
curstate
in
...
...
@@ -2263,8 +2275,8 @@ and (to_reactive_prg_ldbg :
in
let
(
cont2
:
Event
.
ctx
->
behavior
->
Event
.
t
)
=
fun
ctx
b
->
match
b
with
|
Raise
x
->
raise
(
Exception
x
)
|
Vanish
->
r
ai
se
Stop
|
Raise
x
->
excn_cont
ctx
x
|
Vanish
->
f
ai
l_cont
ctx
|
Goto
(
zeguard
,
ctrl'
)
->
(* THIS IS THE NORMAL BEHAVIOR *)
let
(
outs
,
locs
)
=
...
...
@@ -2343,7 +2355,7 @@ and (to_reactive_prg_ldbg :
Event
.
inputs
=
ctx
.
Event
.
ctx_inputs
;
Event
.
outputs
=
ctx
.
Event
.
ctx_outputs
;
Event
.
data
=
edata
@
predata
;
Event
.
next
=
(
fun
()
->
genpath_ldbg
it
data
cstate
ctx
cont2
fail_cont
);
Event
.
next
=
(
fun
()
->
genpath_ldbg
it
data
cstate
ctx
cont2
fail_cont
excn_cont
);
Event
.
terminate
=
ctx
.
Event
.
ctx_terminate
;
Event
.
sinfo
=
None
;
}
...
...
@@ -2375,16 +2387,14 @@ let get_behavior_gen_ldbg : t -> Var.env_in -> Var.env -> control_state -> Event
(* prépare les params pour l'appel de la fct. rec. de parcours de trace
on part du principe qu'on a la meme interface que le genpath (?)
*)
(* try *)
let
data
=
{
curs
=
ins
;
pres
=
pres
}
in
let
cont2
ctx
(
b
:
behavior
)
=
let
and_thats_all
()
=
NoMoreBehavior
0
in
cont
ctx
(
SomeBehavior
(
b
,
and_thats_all
))
in
let
fail_cont
_ctx
=
failwith
(
"deadlock"
)
in
genpath_ldbg
it
data
cstate
ctx
cont2
fail_cont
(* with DeadlockE (e,ctx) -> NoMoreBehavior 0 *)
(* raise (Event.Error ("deadlock", e)) *)
let
excn_cont
ctx
x
=
failwith
(
"Lutin Exception "
^
x
)
in
genpath_ldbg
it
data
cstate
ctx
cont2
fail_cont
excn_cont
(***************************************************************************************)
...
...
lutin/src/mainArg.ml
View file @
bf5cb12d
...
...
@@ -110,10 +110,10 @@ let event_incr opt =
let
r
=
Random
.
int
1073741823
in
opt
._
event_nb
<-
opt
._
event_nb
+
1
;
Random
.
full_init
[
|
seed
;
opt
._
event_nb
|
];
Printf
.
fprintf
stderr
"The random engine seed is set with (%i,%i) (%i,%i)
\n
"
opt
._
event_nb
seed
r
(
Random
.
int
1073741823
);
flush
stderr
;
(*
Printf.fprintf
*)
(*
stderr "The random engine seed is set with (%i,%i) (%i,%i)\n"
*)
(*
opt._event_nb seed r (Random.int 1073741823);
*)
(*
flush stderr;
*)
()
...
...
lutin/src/reactive.ml
View file @
bf5cb12d
...
...
@@ -8,12 +8,13 @@ let step p = match p with DoStep _p -> _p
type
prg_ldbg
=
DoStep_ldbg
of
(
Event
.
ctx
->
Value
.
t
list
->
(
Event
.
ctx
->
prg_ldbg
->
Value
.
t
list
->
Event
.
t
)
->
(
Event
.
ctx
->
Event
.
t
)
->
Event
.
t
)
(
Event
.
ctx
->
Event
.
t
)
->
(
Event
.
ctx
->
string
->
Event
.
t
)
->
Event
.
t
)
let
(
step_ldbg
:
Event
.
ctx
->
prg_ldbg
->
Value
.
t
list
->
(
Event
.
ctx
->
prg_ldbg
->
Value
.
t
list
->
Event
.
t
)
->
(
Event
.
ctx
->
Event
.
t
)
->
Event
.
t
)
=
->
(
Event
.
ctx
->
Event
.
t
)
->
(
Event
.
ctx
->
string
->
Event
.
t
)
->
Event
.
t
)
=
fun
ctx
p
vl
cont
fail_cont
->
match
p
with
DoStep_ldbg
_p
->
_p
ctx
vl
cont
fail_cont
lutin/src/reactive.mli
View file @
bf5cb12d
...
...
@@ -8,10 +8,11 @@ val step : prg -> Value.t list -> (Value.t list * prg)
type
prg_ldbg
=
DoStep_ldbg
of
(
Event
.
ctx
->
Value
.
t
list
->
(
Event
.
ctx
->
prg_ldbg
->
Value
.
t
list
->
Event
.
t
)
->
(
Event
.
ctx
->
Event
.
t
)
->
Event
.
t
)
(
Event
.
ctx
->
Event
.
t
)
->
(
Event
.
ctx
->
string
->
Event
.
t
)
->
Event
.
t
)
val
step_ldbg
:
Event
.
ctx
->
prg_ldbg
->
Value
.
t
list
->
(
Event
.
ctx
->
prg_ldbg
->
Value
.
t
list
->
Event
.
t
)
->
(
Event
.
ctx
->
Event
.
t
)
->
Event
.
t