Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
verimag
synchrone
lutin
Commits
c2eb6c77
Commit
c2eb6c77
authored
Apr 10, 2019
by
erwan
Browse files
Update: monadisation of Lutin, part 1.
Rationale: make rdbg time traveling work.
parent
43c4caa9
Changes
3
Hide whitespace changes
Inline
Side-by-side
lutin/src/lutProg.ml
View file @
c2eb6c77
...
...
@@ -12,6 +12,7 @@ Interface avec les modules lucky :
open
LutErrors
open
Exp
open
Value
open
Util
type
lucky_var
=
Exp
.
var
...
...
@@ -20,16 +21,16 @@ let dbg = Verbose.get_flag "LutProg"
type
t
=
{
auto
:
AutoGen
.
t
;
(* table : string -> lucky_var for compiling *)
lucky_var_tab
:
(
string
,
lucky_var
)
Hashtbl
.
t
;
lucky_prevar_tab
:
(
string
,
lucky_var
)
Hashtbl
.
t
;
lucky_var_tab
:
lucky_var
StringMap
.
t
;
lucky_prevar_tab
:
lucky_var
StringMap
.
t
;
}
(* set the pre_tab of a LutProg.t associated to a ... *)
let
create
a
=
{
auto
=
a
;
lucky_var_tab
=
Hashtbl
.
create
50
;
lucky_prevar_tab
=
Hashtbl
.
create
50
;
lucky_var_tab
=
StringMap
.
empty
;
lucky_prevar_tab
=
StringMap
.
empty
;
}
(* CONVERSION TYPE LUTIN -> TYPE LUCKY (CkTypeEff.t -> Type.t) *)
...
...
@@ -60,7 +61,7 @@ let lucky_exp_var_ref (x:lucky_var) = (
let
lucky_ref_of
?
(
where
=
""
)
tab
nme
=
(
try
(
lucky_exp_var_ref
(
Util
.
hfind
tab
nme
)
lucky_exp_var_ref
(
StringMap
.
find
nme
tab
)
)
with
Not_found
->
(
raise
(
LutErrors
.
Internal_error
(
...
...
@@ -254,11 +255,11 @@ let add_pre (it:t) (x:lucky_var) = (
let
nme
=
Var
.
name
x
in
(* Verbose.put ~flag:dbg " LutProg.add_pre \"%s\"\n" nme; *)
try
(
Util
.
h
find
it
.
lucky_prevar_tab
nme
StringMap
.
find
nme
it
.
lucky_prevar_tab
,
it
)
with
Not_found
->
(
let
prex
=
Var
.
make_pre
x
in
Hashtbl
.
add
it
.
lucky_prevar_tab
nme
prex
;
prex
let
it
=
{
it
with
lucky_prevar_tab
=
StringMap
.
add
nme
prex
it
.
lucky_prevar_tab
}
in
prex
,
it
)
)
...
...
@@ -291,106 +292,114 @@ let lucky_make_var it mnode nme ty mode range_opt = (
)
let
init_vars
(
it
:
t
)
=
(
let
auto
=
it
.
auto
in
let
source_code
=
AutoGen
.
source
auto
in
let
mnode
=
Expand
.
node_name
source_code
in
(***********************************************************)
(*************** FONCTIONS EXTERNES ************************)
(***********************************************************)
(* ICI -> A FAIRE ??
let etab2prof s xi acc = (
(s, xi.xi_prof)::acc
) in
let xlist = Hashtbl.fold etab2prof
(Expand.extern_tab source_code) [] in
if (xlist = []) then ()
else (
fprintf os "\nfunctions {\n";
let pxd (s, p) = (
fprintf os " %s : %s;\n" s (CkTypeEff.prof_to_string p)
) in
List.iter pxd xlist;
fprintf os "}\n";
);
*)
(***********************************************************)
(*************** VARIABLES *********************************)
(***********************************************************)
let
add_support
mode
id
=
(
let
nme
=
CoIdent
.
to_string
id
in
let
info
=
Util
.
hfind
(
Expand
.
support_tab
source_code
)
id
in
(* Verbose.put ~flag:dbg " LutProg.add_support \"%s\"\n" nme; *)
let
res
=
lucky_make_var
it
mnode
nme
(
lucky_type_of
info
.
Expand
.
si_type
)
mode
info
.
Expand
.
si_range
in
(* init ? *)
let
res
=
match
info
.
Expand
.
si_init
with
let
auto
=
it
.
auto
in
let
source_code
=
AutoGen
.
source
auto
in
let
mnode
=
Expand
.
node_name
source_code
in
(***********************************************************)
(*************** FONCTIONS EXTERNES ************************)
(***********************************************************)
(* ICI -> A FAIRE ??
let etab2prof s xi acc = (
(s, xi.xi_prof)::acc
) in
let xlist = Hashtbl.fold etab2prof
(Expand.extern_tab source_code) [] in
if (xlist = []) then ()
else (
fprintf os "\nfunctions {\n";
let pxd (s, p) = (
fprintf os " %s : %s;\n" s (CkTypeEff.prof_to_string p)
) in
List.iter pxd xlist;
fprintf os "}\n";
);
*)
(***********************************************************)
(*************** VARIABLES *********************************)
(***********************************************************)
let
add_support
mode
it
id
=
(
let
nme
=
CoIdent
.
to_string
id
in
let
info
=
Util
.
hfind
(
Expand
.
support_tab
source_code
)
id
in
(* Verbose.put ~flag:dbg " LutProg.add_support \"%s\"\n" nme; *)
let
res
=
lucky_make_var
it
mnode
nme
(
lucky_type_of
info
.
Expand
.
si_type
)
mode
info
.
Expand
.
si_range
in
(* init ? *)
let
res
=
match
info
.
Expand
.
si_init
with
|
None
->
res
|
Some
e
->
Var
.
set_init
res
(
lucky_exp_of
(
compil_id2exp
it
)
e
)
in
(* default ? *)
let
res
=
match
info
.
Expand
.
si_default
with
in
(* default ? *)
let
res
=
match
info
.
Expand
.
si_default
with
|
None
->
res
|
Some
e
->
Var
.
set_default
res
(
lucky_exp_of
(
compil_id2exp
it
)
e
)
in
(* le pre est utilis qq part <=> le champ si_pre_ref_exp est renseign *)
let
_
=
match
info
.
Expand
.
si_pre_ref_exp
with
|
Some
e
->
let
_
=
add_pre
it
res
in
()
|
None
->
()
in
Hashtbl
.
add
it
.
lucky_var_tab
nme
res
)
in
let
add_alias
id
=
(
let
nme
=
CoIdent
.
to_string
id
in
Verbose
.
put
~
flag
:
dbg
" LutProg.add_alias
\"
%s
\"\n
"
nme
;
let
info
=
Util
.
hfind
(
Expand
.
alias_tab
source_code
)
id
in
(* les alias sont des Local spciaux en lucky *)
let
res
=
Var
.
set_alias
(
lucky_make_var
it
mnode
nme
(
lucky_type_of
info
.
Expand
.
ai_type
)
Var
.
Local
None
)
(
lucky_exp_of
(
compil_id2exp
it
)
info
.
Expand
.
ai_def_exp
)
in
Hashtbl
.
add
it
.
lucky_var_tab
nme
res
)
in
in
(* le pre est utilis qq part <=> le champ si_pre_ref_exp est renseign *)
let
_
=
match
info
.
Expand
.
si_pre_ref_exp
with
|
Some
e
->
let
_
,
it
=
add_pre
it
res
in
it
|
None
->
it
in
{
it
with
lucky_var_tab
=
StringMap
.
add
nme
res
it
.
lucky_var_tab
}
)
in
let
add_alias
it
id
=
(
let
nme
=
CoIdent
.
to_string
id
in
Verbose
.
put
~
flag
:
dbg
" LutProg.add_alias
\"
%s
\"\n
"
nme
;
let
info
=
Util
.
hfind
(
Expand
.
alias_tab
source_code
)
id
in
(* les alias sont des Local spciaux en lucky *)
let
res
=
Var
.
set_alias
(
lucky_make_var
it
mnode
nme
(
lucky_type_of
info
.
Expand
.
ai_type
)
Var
.
Local
None
)
(
lucky_exp_of
(
compil_id2exp
it
)
info
.
Expand
.
ai_def_exp
)
in
{
it
with
lucky_var_tab
=
StringMap
.
add
nme
res
it
.
lucky_var_tab
}
)
in
(* Loop counters are special local vars.
"i" is the (unique) index of an expression loopi/loopa
N.B. i in [0 , CoTraceExp.nb_loops ()[
*)
let
add_counter
it
(
i
:
int
)
=
(
let
id
=
CoIdent
.
of_cpt
i
in
let
nme
=
CoIdent
.
to_string
id
in
Verbose
.
put
~
flag
:
dbg
" LutProg.add_counter
\"
%s
\"\n
"
nme
;
let
x
=
lucky_make_var
it
mnode
nme
(
lucky_type_of
CkTypeEff
.
integer
)
Var
.
Local
None
in
let
x
=
Var
.
set_init
x
lucky_exp_zero
in
(* par defaut : pre cpt *)
let
px
,
it
=
add_pre
it
x
in
let
x
=
Var
.
set_default
x
(
lucky_exp_var_ref
px
)
in
{
it
with
lucky_var_tab
=
StringMap
.
add
nme
x
it
.
lucky_var_tab
}
)
in
(* ENTRES *)
let
it
=
List
.
fold_left
(
add_support
Var
.
Input
)
it
(
Expand
.
input_list
source_code
)
in
(* Loop counters are special local vars.
"i" is the (unique) index of an expression loopi/loopa
N.B. i in [0 , CoTraceExp.nb_loops ()[
*)
let
add_counter
(
i
:
int
)
=
(
let
id
=
CoIdent
.
of_cpt
i
in
let
nme
=
CoIdent
.
to_string
id
in
Verbose
.
put
~
flag
:
dbg
" LutProg.add_counter
\"
%s
\"\n
"
nme
;
let
x
=
lucky_make_var
it
mnode
nme
(
lucky_type_of
CkTypeEff
.
integer
)
Var
.
Local
None
in
let
x
=
Var
.
set_init
x
lucky_exp_zero
in
(* par defaut : pre cpt *)
let
px
=
add_pre
it
x
in
let
x
=
Var
.
set_default
x
(
lucky_exp_var_ref
px
)
in
Hashtbl
.
add
it
.
lucky_var_tab
nme
x
;
)
in
(* ENTRES *)
List
.
iter
(
add_support
Var
.
Input
)
(
Expand
.
input_list
source_code
);
(* SORTIES *)
List
.
iter
(
add_support
Var
.
Output
)
(
Expand
.
output_list
source_code
);
(* LOCALES support *)
List
.
iter
(
add_support
Var
.
Local
)
(
Expand
.
local_out_list
source_code
);
(* ALIAS (de source_code) *)
List
.
iter
add_alias
(
Expand
.
alias_list
source_code
);
(* Loop counters :
2010/11 -> the creation of loop counters is no longer
make in AutoExlore, since it is NOT compatible with the
lazy exploration.
Now -> counters are created A PRIORI, one for each loopa/loopi
created during Expand.
*)
(* List.iter add_counter (AutoGen.counters auto); *)
for
i
=
0
to
(
CoTraceExp
.
nb_loops
()
-
1
)
do
add_counter
i
done
(* SORTIES *)
let
it
=
List
.
fold_left
(
add_support
Var
.
Output
)
it
(
Expand
.
output_list
source_code
);
in
(* LOCALES support *)
let
it
=
List
.
fold_left
(
add_support
Var
.
Local
)
it
(
Expand
.
local_out_list
source_code
);
in
(* ALIAS (de source_code) *)
let
it
=
List
.
fold_left
add_alias
it
(
Expand
.
alias_list
source_code
);
in
(* Loop counters :
2010/11 -> the creation of loop counters is no longer
make in AutoExlore, since it is NOT compatible with the
lazy exploration.
Now -> counters are created A PRIORI, one for each loopa/loopi
created during Expand.
*)
(* List.iter add_counter (AutoGen.counters auto); *)
let
it_ref
=
ref
it
in
for
i
=
0
to
(
CoTraceExp
.
nb_loops
()
-
1
)
do
it_ref
:=
add_counter
!
it_ref
i
done
;
!
it_ref
)
(*
...
...
@@ -432,10 +441,7 @@ N.B. in simu mode, pre's are not handled by lucky but zelut !
extract the necessary pre's
from a triple of current input, out and loc,
*)
let
make_pre_env
(
zelut
:
t
)
ins
outs
locs
=
(
let
pl
=
zelut
.
lucky_prevar_tab
in
let
make_pre_env
(
zelut
:
t
)
ins
outs
locs
=
(* DON'T FAIL here ! will fail in eval if pre's are actually used
let error what who = raise (
Internal_error ("AutoGen.make_pre_env",
...
...
@@ -443,11 +449,11 @@ let make_pre_env (zelut:t) ins outs locs = (
)
) in
*)
let
dopre
nme
lucvar
acc
=
(
let
lvt
=
zelut
.
lucky_var_tab
in
let
dopre
nme
lucvar
acc
=
Verbose
.
put
~
flag
:
dbg
"%% make_pre_ena/dopre
\"
%s
\"
"
nme
;
try
(
let
zevar
=
Util
.
hfind
zelut
.
lucky_var_tab
nme
in
let
zevar
=
StringMap
.
find
nme
lvt
in
let
tab
=
match
(
Var
.
mode
zevar
)
with
|
Var
.
Input
->
ins
|
Var
.
Output
->
outs
...
...
@@ -457,9 +463,9 @@ let make_pre_env (zelut:t) ins outs locs = (
let
value
=
Value
.
OfIdent
.
get
tab
nme
in
Value
.
OfIdent
.
add
acc
(
nme
,
value
)
)
with
Not_found
->
acc
)
in
Hashtbl
.
fold
dopre
pl
Value
.
OfIdent
.
empty
)
in
let
pre_values
=
StringMap
.
fold
dopre
zelut
.
lucky_prevar_tab
Value
.
OfIdent
.
empty
in
pre_values
let
lut_get_wtl
(
zelut
:
t
)
(
input
:
Var
.
env_in
)
(
st
:
Prog
.
state
)
(
ctrlst
:
Prog
.
ctrl_state
)
=
(
...
...
@@ -597,10 +603,10 @@ let make ?(libs: string list option = None) infile mnode = (
Verbose
.
put
~
level
:
3
"#---end AutoGen.make
\n
"
;
let
zelut
=
create
auto
in
let
_
=
init_vars
zelut
in
let
zelut
=
init_vars
zelut
in
let
id2var
(
id
:
CoIdent
.
t
)
=
let
nme
=
CoIdent
.
to_string
id
in
Util
.
hfind
zelut
.
lucky_var_tab
nme
StringMap
.
find
nme
zelut
.
lucky_var_tab
in
let
sort_bool_num
k
v
(
blin
,
nlin
)
=
(* Verbose.exe ~level:3 (fun () -> Printf.fprintf stderr "sort_bool_num %s=%s\n" k (Var.to_string v)); *)
...
...
@@ -615,10 +621,10 @@ let make ?(libs: string list option = None) infile mnode = (
)
|
_
->
(
blin
,
nlin
)
in
let
(
bl
,
nl
)
=
Hashtbl
.
fold
sort_bool_num
zelut
.
lucky_var_tab
([]
,
[]
)
in
let
(
bl
,
nl
)
=
StringMap
.
fold
sort_bool_num
zelut
.
lucky_var_tab
([]
,
[]
)
in
(* let get_all_mems n ve a = (n,ve)::a in *)
(* let get_all_mems n ve a = (Prevar.get_pre_var_name n, ve)::a in *)
let
get_all_mems
n
ve
a
=
(
Var
.
name
ve
,
Util
.
h
find
zelut
.
lucky_var_tab
n
)
::
a
in
let
get_all_mems
n
ve
a
=
(
Var
.
name
ve
,
StringMap
.
find
n
zelut
.
lucky_var_tab
)
::
a
in
(* la fonction qui dit si c'est final *)
let
is_final
s
=
match
AutoGen
.
get_state_info
zelut
.
auto
s
with
...
...
@@ -633,7 +639,7 @@ let make ?(libs: string list option = None) infile mnode = (
Prog
.
out_vars
=
List
.
map
id2var
(
Expand
.
output_list
exped
);
Prog
.
loc_vars
=
List
.
map
id2var
(
Expand
.
local_out_list
exped
);
Prog
.
ext_func_tbl
=
Util
.
StringMap
.
empty
;
Prog
.
memories_names
=
Hashtbl
.
fold
get_all_mems
zelut
.
lucky_prevar_tab
[]
;
Prog
.
memories_names
=
StringMap
.
fold
get_all_mems
zelut
.
lucky_prevar_tab
[]
;
Prog
.
bool_vars_to_gen
=
[
bl
];
Prog
.
num_vars_to_gen
=
[
nl
];
Prog
.
output_var_names
=
[
Expand
.
output_list
exped
];
...
...
@@ -657,40 +663,43 @@ let make ?(libs: string list option = None) infile mnode = (
)
let
get_init_state
?
(
verb_level
=
0
)
zelutprog
zeprog
=
(
let
get_init_vals
accin
lucvar
=
(
let
nme
=
Var
.
name
lucvar
in
match
Var
.
init
lucvar
with
|
None
->
accin
|
Some
e
->
(
let
v
=
match
e
with
|
Formu
True
->
B
true
|
Formu
False
->
B
false
|
Numer
(
Ival
i
)
->
N
(
I
i
)
|
Numer
(
Fval
r
)
->
N
(
F
r
)
|
Numer
(
Uminus
(
Ival
i
))
->
N
(
I
(
Num
.
minus_num
i
))
|
Numer
(
Uminus
(
Fval
r
))
->
N
(
F
(
-.
r
))
|
_
->
raise
(
Internal_error
(
"LutProg.get_init_state"
,
(
"initial value of
\"
"
^
nme
^
"
\"
must be a constant expression"
^
" (but get "
^
(
Exp
.
to_string
e
)
^
")"
)
))
in
Value
.
OfIdent
.
add
accin
(
nme
,
v
)
let
get_init_vals
accin
lucvar
=
(
let
nme
=
Var
.
name
lucvar
in
match
Var
.
init
lucvar
with
|
None
->
accin
|
Some
e
->
(
let
v
=
match
e
with
|
Formu
True
->
B
true
|
Formu
False
->
B
false
|
Numer
(
Ival
i
)
->
N
(
I
i
)
|
Numer
(
Fval
r
)
->
N
(
F
r
)
|
Numer
(
Uminus
(
Ival
i
))
->
N
(
I
(
Num
.
minus_num
i
))
|
Numer
(
Uminus
(
Fval
r
))
->
N
(
F
(
-.
r
))
|
_
->
raise
(
Internal_error
(
"LutProg.get_init_state"
,
(
"initial value of
\"
"
^
nme
^
"
\"
must be a constant expression"
^
" (but get "
^
(
Exp
.
to_string
e
)
^
")"
)
))
in
Value
.
OfIdent
.
add
accin
(
nme
,
v
)
)
)
in
{
Prog
.
s
=
zeprog
;
Prog
.
d
=
{
Prog
.
memory
=
Value
.
OfIdent
.
empty
;
Prog
.
ctrl_state
=
zeprog
.
Prog
.
initial_ctrl_state
;
(* Prog.last_input = Value.OfIdent.empty; *)
(* Prog.last_output = Value.OfIdent.empty; *)
(* Prog.last_local = Value.OfIdent.empty; *)
Prog
.
last_input
=
List
.
fold_left
get_init_vals
Value
.
OfIdent
.
empty
(
zeprog
.
Prog
.
in_vars
);
Prog
.
last_output
=
List
.
fold_left
get_init_vals
Value
.
OfIdent
.
empty
(
zeprog
.
Prog
.
out_vars
);
Prog
.
last_local
=
List
.
fold_left
get_init_vals
Value
.
OfIdent
.
empty
(
zeprog
.
Prog
.
loc_vars
);
Prog
.
verbose
=
verb_level
}
}
)
in
{
Prog
.
s
=
zeprog
;
Prog
.
d
=
{
Prog
.
memory
=
Value
.
OfIdent
.
empty
;
Prog
.
ctrl_state
=
zeprog
.
Prog
.
initial_ctrl_state
;
(* Prog.last_input = Value.OfIdent.empty; *)
(* Prog.last_output = Value.OfIdent.empty; *)
(* Prog.last_local = Value.OfIdent.empty; *)
Prog
.
last_input
=
List
.
fold_left
get_init_vals
Value
.
OfIdent
.
empty
(
zeprog
.
Prog
.
in_vars
);
Prog
.
last_output
=
List
.
fold_left
get_init_vals
Value
.
OfIdent
.
empty
(
zeprog
.
Prog
.
out_vars
);
Prog
.
last_local
=
List
.
fold_left
get_init_vals
Value
.
OfIdent
.
empty
(
zeprog
.
Prog
.
loc_vars
);
Prog
.
verbose
=
verb_level
}
}
)
(* renvoie le state initial facon Prog *)
let
make_state
?
(
libs
:
string
list
option
=
None
)
?
(
verb_level
=
0
)
infile
mnode
=
(
...
...
lutin/src/lutProg.mli
View file @
c2eb6c77
...
...
@@ -8,6 +8,7 @@ val make : ?libs:string list option -> string list -> string -> (t * Prog.t)
val
get_init_state
:
?
verb_level
:
int
->
t
->
Prog
.
t
->
Prog
.
state
(** [make_state infile mnode] *)
val
make_state
:
?
libs
:
string
list
option
->
?
verb_level
:
int
->
string
list
->
string
->
Prog
.
state
val
make_state
:
?
libs
:
string
list
option
->
?
verb_level
:
int
->
string
list
->
string
->
Prog
.
state
(* val fomula_of : Var.env -> Var.env -> CoAlgExp.t -> Exp.formula *)
lutin/src/main.ml
View file @
c2eb6c77
...
...
@@ -126,8 +126,9 @@ let rec to_simu oc infile mnode opt = (
let
state0
=
LutProg
.
get_init_state
zelutprog
zeprog
in
let
init_state_dyn
=
{
state0
.
Prog
.
d
with
Prog
.
verbose
=
Verbose
.
level
()
}
in
let
init_state
=
{
state0
with
Prog
.
d
=
init_state_dyn
}
in
let
loc
=
if
(
MainArg
.
show_locals
opt
)
then
Some
init_state
.
Prog
.
s
.
Prog
.
loc_vars
else
None
in
let
loc
=
if
(
MainArg
.
show_locals
opt
)
then
Some
init_state
.
Prog
.
s
.
Prog
.
loc_vars
else
None
in
let
seed
=
MainArg
.
seed
opt
in
let
msg
=
Printf
.
sprintf
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment