Commit b235802a authored by Pascal Raymond's avatar Pascal Raymond
Browse files

lutexe: init vals of in/outs seems to work

parent 1504bb64
......@@ -345,7 +345,7 @@ let new_support_input
si_src = src;
si_default = None;
si_scope = None;
si_init = None;
si_init = init;
si_range = None;
};
(* on garde la liste pour les sortir dans l'ordre *)
......@@ -357,8 +357,8 @@ let new_support_input
(* output (de node) => on garde l'ident, contrôlable *)
let new_support_output
(* info optionnelles *)
?(init: CoAlgExp.t option = None)
(range_opt: (CoAlgExp.t * CoAlgExp.t) option)
(init: CoAlgExp.t option)
(range_opt: (CoAlgExp.t * CoAlgExp.t) option)
(i : Syntaxe.ident)
(t : Syntaxe.type_exp)
(sstack : CoIdent.scope_stack) =
......@@ -391,9 +391,9 @@ let new_support_output
(* local (de node) => on garde l'ident, contrôlable *)
let new_support_local
(* info optionnelles *)
?(init: CoAlgExp.t option = None)
?(scope: support_scope option = None)
(range_opt: (CoAlgExp.t * CoAlgExp.t) option)
(scope: support_scope option)
(init: CoAlgExp.t option)
(range_opt: (CoAlgExp.t * CoAlgExp.t) option)
(* info générales *)
(i : Syntaxe.ident)
(t : Syntaxe.type_exp)
......@@ -1204,7 +1204,7 @@ and
let zescope = new_support_scope src_scope in
(* ... then filled by added var one by one *)
let f = function (i, t, ivopt, range_opt) -> (
new_support_local ~scope:(Some zescope) ~init:ivopt range_opt i t sstack
new_support_local (Some zescope) ivopt range_opt i t sstack
) in
List.iter f newidlist;
(* on continu dans ce nouvel env ... *)
......@@ -1463,7 +1463,7 @@ let make (env : CheckEnv.t) (p : Syntaxe.package) (n : string) = (
(ni.ndi_outputs)
in
let add_output = function (i, t, vopt, range_opt) -> (
new_support_output ~init:vopt range_opt i t sstack
new_support_output vopt range_opt i t sstack
) in
List.iter add_output outlist;
......@@ -1533,6 +1533,22 @@ let dump (x:t) = (
| None -> printf "(not defined)"
| Some e -> CoAlgExp.dump e
in
printf "\n init : ";
let _ = match si.si_init with
| None -> printf "(not defined)"
| Some e -> CoAlgExp.dump e
in
printf "\n range : ";
let _ = match si.si_range with
| None -> printf "(not defined)"
| Some (e1,e2) -> (
printf "[ ";
CoAlgExp.dump e1;
printf " ; ";
CoAlgExp.dump e2;
printf "]";
)
in
printf "\n src :\n" ;
CoIdent.print_src_stack si.si_src ;
printf "\n" ;
......
......@@ -52,7 +52,7 @@ let lucky_exp_var_ref (x: Exp.var) = (
N.B. partial eval is defined in another module
*)
type id2exp = CoAlgExp.node -> Exp.t
type id2exp = bool -> CoAlgExp.node -> Exp.t
let lucky_exp_of (eval:bool) (id2exp:id2exp) (e: CoAlgExp.t) = (
......@@ -78,7 +78,7 @@ let lucky_exp_of (eval:bool) (id2exp:id2exp) (e: CoAlgExp.t) = (
| CoAlgExp.AE_pre id
| CoAlgExp.AE_support id
| CoAlgExp.AE_alias id -> (
match id2exp nat with
match id2exp eval nat with
| Exp.Formu f -> f
| _ -> (
raise (
......@@ -144,7 +144,7 @@ let lucky_exp_of (eval:bool) (id2exp:id2exp) (e: CoAlgExp.t) = (
| CoAlgExp.AE_pre id
| CoAlgExp.AE_support id
| CoAlgExp.AE_alias id -> (
match id2exp nat with
match id2exp eval nat with
| Exp.Numer n -> n
| _ -> (
print_string (
......@@ -220,7 +220,7 @@ Utils.time_R "lucky_formula_of";
)
*)
let lucky_var_of (si : Expand.support_info) = (
let lucky_var_of (id2exp: id2exp)(si : Expand.support_info) = (
let nme = CoIdent.to_string si.Expand.si_ident in
let ty = lucky_type_of si.Expand.si_type in
let mode = match si.Expand.si_nature with
......@@ -230,13 +230,27 @@ let lucky_var_of (si : Expand.support_info) = (
in
let res = Var.make "" nme ty mode in
(* HERE: store it ??? *)
(* init ? *)
let res = match si.Expand.si_init with
| None -> res
| Some e -> Var.set_init res (lucky_exp_of true id2exp e)
in
(* range ? *)
let res = match si.Expand.si_range with
| None -> res
| Some (low, high) ->
let res = Var.set_min res (lucky_exp_of true id2exp low) in
let res = Var.set_max res (lucky_exp_of true id2exp high) in
res
in
res
)
(* check FULL satisfiability
of a formula CONTAINING ONLY CONTROLABLE VARS
for the time being, just a simplified version of Solver.solve_formula
*)
does not work ...
let check_satisfiablity (f:Exp.formula) = (
(* builds the bdd ... *)
......@@ -268,3 +282,4 @@ let check_satisfiablity (f:Exp.formula) = (
(sols <> [])
)
)
*)
......@@ -15,20 +15,22 @@ val lucky_exp_of_int : int -> Exp.t
val lucky_exp_of_float : float -> Exp.t
val lucky_exp_of_value : Value.t -> Exp.t
(* lutin support var to lucky var *)
val lucky_var_of : Expand.support_info -> Exp.var
(* lucky var to its reference exp *)
val lucky_exp_var_ref : Exp.var -> Exp.t
(* translators CoAlgExp to Exp take as argument
the function in charge of translating ident refs:
the argument MUST be a id ref (AE_pre, AE_support, AE_alias)
first arg true -> partial eval
*)
type id2exp = CoAlgExp.node -> Exp.t
type id2exp = bool -> CoAlgExp.node -> Exp.t
(* lutin support var to lucky var *)
val lucky_var_of : id2exp -> Expand.support_info -> Exp.var
(* translator lutin exp -> lucky exp *)
val lucky_exp_of : bool -> id2exp -> CoAlgExp.t -> Exp.t
val check_satisfiablity : Exp.formula -> bool
(* val check_satisfiablity : Exp.formula -> bool *)
......@@ -59,8 +59,13 @@ type support = Exp.var list * Exp.var list
type t = {
expanded_code: Expand.t;
(* translation CoIdent -> Exp.var is done once *)
in_vars: Exp.var list;
out_vars: Exp.var list;
loc_vars: Exp.var list;
(* (partial) initial values of global vars (ins/outs *)
init_pres: Value.OfIdent.t;
id2var_tab: (string, Exp.var) Hashtbl.t;
(* REQUIRED BY SolveR.solve_formula *)
(* list of names for outputs ... *)
......@@ -71,32 +76,61 @@ type t = {
num_vars_to_gen: Exp.var list;
}
let in_var_list it = it.in_vars
let out_var_list it = it.out_vars
let loc_var_list it = it.loc_vars
(* utils: translation lucky/lutin is made in Glue
everything that depends on Expand.t is made here
*)
let id2var (xenv: Expand.t) (id:CoIdent.t) = (
let info = Hashtbl.find (Expand.support_tab xenv) id in
Glue.lucky_var_of info
)
(** standard id2exp to use with Glue.lucky_exp_of
(** standard unalias id2exp to use with Glue.lucky_exp_of
NO PARTIAL EVAL
*)
let rec id2exp (it:t) (idref:CoAlgExp.node) = (
let rec unalias (it:t) (eval:bool) (idref:CoAlgExp.node) = (
match idref with
| CoAlgExp.AE_alias id -> (
(* let nme = CoIdent.to_string id in *)
let xenv = it.expanded_code in
(* let nme = CoIdent.to_string id in *)
let e = (Hashtbl.find (Expand.alias_tab xenv) id).Expand.ai_def_exp in
Glue.lucky_exp_of false (id2exp it) e
Glue.lucky_exp_of eval (unalias it) e
)
| CoAlgExp.AE_support id -> (
Glue.lucky_exp_var_ref (id2var it.expanded_code id)
Glue.lucky_exp_var_ref (id2var it id)
)
| CoAlgExp.AE_pre id -> assert false
| _ -> assert false
)
(** static unalias id2exp to use with Glue.lucky_exp_of
NO PARTIAL EVAL, NO SUPPORT VAR
*)
and static_unalias (xenv:Expand.t) (eval:bool) (idref:CoAlgExp.node) = (
match idref with
| CoAlgExp.AE_alias id -> (
(* let nme = CoIdent.to_string id in *)
let e = (Hashtbl.find (Expand.alias_tab xenv) id).Expand.ai_def_exp in
Glue.lucky_exp_of eval (static_unalias xenv) e
)
| CoAlgExp.AE_support id -> assert false
| CoAlgExp.AE_pre id -> assert false
| _ -> assert false
)
(* store new var *)
and new_id2var
(tab: (string, Exp.var) Hashtbl.t)
(xenv: Expand.t)
(id:CoIdent.t) =
(
let info = Hashtbl.find (Expand.support_tab xenv) id in
let var = Glue.lucky_var_of (static_unalias xenv) info in
Hashtbl.add tab id var;
var
)
and id2var (it:t) (id:CoIdent.t) = (
(* let info = Hashtbl.find (Expand.support_tab xenv) id in *)
(* Glue.lucky_var_of unalias info *)
Hashtbl.find it.id2var_tab id
)
let make ?(libs: string list option = None) infile mnode = (
try (
......@@ -120,10 +154,15 @@ let make ?(libs: string list option = None) infile mnode = (
mnode
) in
let exped = Expand.make tlenv mainprg mnode in
let id2var_tab = Hashtbl.create 10 in
(* lucky-like vars are created once for all *)
let ovs = List.map (id2var exped) (Expand.output_list exped) in
let ivs = List.map (new_id2var id2var_tab exped)
(Expand.input_list exped) in
let ovs = List.map (new_id2var id2var_tab exped)
(Expand.output_list exped) in
let ovns = List.map (Var.name) ovs in
let lvs = List.map (id2var exped) (Expand.local_list exped) in
let lvs = List.map (new_id2var id2var_tab exped)
(Expand.local_list exped) in
(* all uncontrolables ... *)
let uvs = ovs @ lvs in
let isbool v = ((Var.typ v) = Type.BoolT) in
......@@ -134,10 +173,24 @@ let make ?(libs: string list option = None) infile mnode = (
| [] -> Exp.True
| h::t -> List.fold_left (fun acc v -> (Exp.And(Exp.Bvar(v), acc))) (Exp.Bvar h) t
in
(* init pres *)
let addpre acc x = (
match Var.init x with
| None -> acc
| Some e -> (
let v = Exp.to_value e in
Value.OfIdent.add acc (Var.name x, v)
)
) in
let ip = List.fold_left addpre (Value.OfIdent.empty) ivs in
let ip = List.fold_left addpre ip ovs in
{
expanded_code = exped;
out_vars = ovs;
in_vars = ivs;
loc_vars = lvs;
id2var_tab = id2var_tab;
init_pres = ip;
out_var_names = ovns;
bool_vars_to_gen = bvf;
num_vars_to_gen = nvs;
......@@ -176,6 +229,8 @@ let get_init_state it = (
init_info.Expand.ti_def_exp
)
let get_init_pres it = it.init_pres
(* Le type guard correspond aux contraintes dans les goto.
Pour l'instant : on utilise Exp.formula
......@@ -196,14 +251,17 @@ let string_of_guard g = (
(* CoAlgExp to (lucky) Exp with:
- unaliasing
- uncontrolable
- partial eval (always)
*)
let rec contextual_id2exp xenv data (idref:CoAlgExp.node) = (
let unalias s = (Hashtbl.find (Expand.alias_tab xenv) s).Expand.ai_def_exp in
let rec contextual_id2exp (it:t) data (eval:bool) (idref:CoAlgExp.node) = (
let unalias s =
(Hashtbl.find (Expand.alias_tab it.expanded_code) s).Expand.ai_def_exp
in
match idref with
| CoAlgExp.AE_alias id -> (
let e' = unalias id in
contextual_lutexp2exp xenv data e'
contextual_lutexp2exp it data e'
)
| CoAlgExp.AE_support id -> (
(* does the value exist in data.curs ? *)
......@@ -211,7 +269,7 @@ let rec contextual_id2exp xenv data (idref:CoAlgExp.node) = (
let v = Value.OfIdent.get data.curs id in
Glue.lucky_exp_of_value v
) with Not_found -> (
Glue.lucky_exp_var_ref (id2var xenv id)
Glue.lucky_exp_var_ref (id2var it id)
) in res
)
| CoAlgExp.AE_pre id -> (
......@@ -228,33 +286,86 @@ let rec contextual_id2exp xenv data (idref:CoAlgExp.node) = (
)
| _ -> assert false
) and
contextual_lutexp2exp xenv data e = (
contextual_lutexp2exp (it:t) data e = (
(* PARTIAL EVAL *)
Glue.lucky_exp_of true (contextual_id2exp xenv data) e
Glue.lucky_exp_of true (contextual_id2exp it data) e
)
exception Deadlock
let add_to_guard xenv data (e:CoAlgExp.t) (acc:guard) = (
(* reuse Solver.solve_formula *)
let find_some_sols : t -> Thickness.formula_draw_nb -> Thickness.numeric -> guard -> (Var.env_out * Var.env_loc) list =
fun it tfdn tn g -> (
(* clean everything in case ? *)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
(* HERE : dont't know exactly why but it seems to be
necessary to call Solver.is_satisfiable first
*)
let solver_vl = ref 0 in
Verbose.exe ~flag:dbg (fun _ -> solver_vl := 3);
let is_bool_sat = Solver.is_satisfiable
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
!solver_vl
"LutExe.is_bool_sat" (* ctx_msg: string *)
g
"LutExe.is_bool_sat" (* msg: string (?) *)
in
let sols = Solver.solve_formula
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
!solver_vl (* vl: int *)
"LutExe.solve_guard" (* msg: string *)
[it.out_var_names] (* output_var_names: Var.name list list *)
tfdn (* p: Thickness.formula_draw_nb *)
tn (* num_thickness Thickness.numeric *)
it.bool_vars_to_gen (* bool_vars_to_gen_f: formula *)
it.num_vars_to_gen (* num_vars_to_gen: var list *)
g (* f: formula *)
in sols
)
let find_one_sol it g = (
match find_some_sols it 1 (1,0,Thickness.AtMost 0) g with
| s::_ -> s
| [] -> raise Not_found
)
(* check_sat *)
let check_satisfiablity (it:t) (f:Exp.formula) = (
try (
Verbose.put ~flag:dbg "--check satisfiablility of \"%s\"\n" (Exp.formula_to_string f);
let _ = find_one_sol it f in
true
) with Not_found -> false
)
let add_to_guard it data (e:CoAlgExp.t) (acc:guard) = (
(* translate e into an Exp.t using lucky_exp_of with an id2exp:
- that performs unalias
- that replace input/pre values
*)
(* necessarily a formula (bool exp), if we rely on type checking ! *)
let le = contextual_lutexp2exp xenv data e in
(* let xenv = it.expanded_code in *)
let le = contextual_lutexp2exp it data e in
let f = match le with
| Exp.Formu f -> f
| _ -> assert false
in
let res = Exp.And (f, acc) in
if (Glue.check_satisfiablity res) then res
if (check_satisfiablity it res) then res
else raise Deadlock
)
(* Tries to compute a value in a context *)
exception Not_a_constant
let compute_exp xenv data e = (
let le = contextual_lutexp2exp xenv data e in
let compute_exp (it:t) data e = (
let le = contextual_lutexp2exp it data e in
try Exp.to_value le
with _ -> raise Not_a_constant
)
......@@ -411,7 +522,7 @@ let genpath
(** Constraint: ~same but solve the conjunction first *)
| TE_constraint ae -> (
try (
let new_acc = add_to_guard xenv data ae acc in
let new_acc = add_to_guard it data ae acc in
cont (Goto (new_acc, TE_eps))
) with Deadlock -> rec_genpath other_brs
)
......@@ -442,7 +553,7 @@ let genpath
| None -> inpres
| Some e -> (
(* first translate to lucky ... *)
let v = try compute_exp xenv data e
let v = try compute_exp it data e
with Not_a_constant _ -> raise (Internal_error ("LutExe.add_pres",
("initial value of \""^id^"\" must be a uncontrolable expression")))
in Value.OfIdent.add inpres (id, v)
......@@ -450,7 +561,7 @@ let genpath
) in
let new_pres = List.fold_left addp data.pres ectx in
let new_data = {data with pres=new_pres} in
rec_genpath ({br with br_data = new_data }::other_brs)
rec_genpath ({br with br_ctrl=te; br_data = new_data }::other_brs)
)
(** Parallel: at least one ? *)
| TE_para ([]) -> assert false
......@@ -740,24 +851,6 @@ fun it ins pres cstate -> (
)
)
(* reuse Solver.solve_formula *)
let solve_guard : t -> Thickness.formula_draw_nb -> Thickness.numeric -> guard -> (Var.env_out * Var.env_loc) list =
fun it tfdn tn g -> (
let sols = Solver.solve_formula
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
0 (* vl: int *)
"LutExe.solve_guard" (* msg: string *)
[it.out_var_names] (* output_var_names: Var.name list list *)
1 (* p: Thickness.formula_draw_nb *)
(1,0,Thickness.AtMost 0) (* num_thickness Thickness.numeric *)
it.bool_vars_to_gen (* bool_vars_to_gen_f: formula *)
it.num_vars_to_gen (* num_vars_to_gen: var list *)
g (* f: formula *)
in sols
)
let make_pre : t -> Var.env_in -> Var.env_out -> Var.env_loc -> Var.env =
fun it ins outs locs -> (
(* for the time being we keep all variables, even if they are not used in a pre ... *)
......@@ -769,4 +862,37 @@ fun it ins outs locs -> (
(*** DEBUG ***)
let dump it = (
Printf.printf "### DUMP LutExe ########################\n";
Printf.printf "### EXPANDED CODE ######################\n";
Expand.dump it.expanded_code;
let var_details x = Var.to_string_verbose Exp.to_string x in
let dump_var x = (
Printf.printf "%s\n" (var_details x)
) in
Printf.printf "### LUCKY INTERFACE ####################\n";
Printf.printf "--- INPUT VARS -------------------------\n";
List.iter dump_var it.in_vars ;
Printf.printf "--- OUTPUT VARS ------------------------\n";
List.iter dump_var it.out_vars ;
Printf.printf "--- LOCAL VARS -------------------------\n";
List.iter dump_var it.loc_vars ;
Printf.printf "--- INITIAL PRE VALUES -----------------\n";
Value.OfIdent.print it.init_pres stdout ;
Printf.printf "--- IDENT 2 LUCKY VARS -----------------\n";
let dump_id2var id x = (
Printf.printf "%s -> (%s)\n" id (var_details x)
) in
Hashtbl.iter dump_id2var it.id2var_tab;
Printf.printf "--- OUPUT IDENT LIST -------------------\n";
Printf.printf "{ %s }\n" (String.concat "; " it.out_var_names);
Printf.printf "--- AND OF CONTROLLABLE BOOL VARS ------\n";
Printf.printf "%s\n" (Exp.formula_to_string it.bool_vars_to_gen);
Printf.printf "--- LIST OF CONTROLLABLE NUM VARS ------\n";
List.iter dump_var it.num_vars_to_gen ;
Printf.printf "\n### END OF DUMP LutExe #################\n\n";
flush stdout;
)
......@@ -44,6 +44,11 @@ type t
val make: ?libs:string list option -> string -> string -> t
(* Misc info *)
val in_var_list: t -> Exp.var list
val out_var_list: t -> Exp.var list
val loc_var_list: t -> Exp.var list
type control_state
type guard
......@@ -61,9 +66,13 @@ type behavior_gen =
val get_init_state: t -> control_state
val get_init_pres: t -> Value.OfIdent.t
val get_behavior_gen : t -> Var.env_in -> Var.env -> control_state -> (unit -> behavior_gen)
val solve_guard : t -> Thickness.formula_draw_nb -> Thickness.numeric -> guard -> (Var.env_out * Var.env_loc) list
val find_some_sols : t -> Thickness.formula_draw_nb -> Thickness.numeric -> guard -> (Var.env_out * Var.env_loc) list
val find_one_sol : t -> guard -> (Var.env_out * Var.env_loc)
(* the "t" is given in order to filter necessary pres, not really necessary *)
val make_pre : t -> Var.env_in -> Var.env_out -> Var.env_loc -> Var.env
......@@ -73,4 +82,5 @@ val make_pre : t -> Var.env_in -> Var.env_out -> Var.env_loc -> Var.env
(* debug *)
val dump : t -> unit
......@@ -674,8 +674,12 @@ let get_init_state ?(verb_level=0) zelutprog zeprog = (
| Formu False -> B false
| Numer (Ival i) -> N (I i)
| Numer (Fval r) -> N (F r)
| Numer (Uminus (Ival i)) -> N (I (-i))
| Numer (Uminus (Fval r)) -> N (F (-.r))
| _ -> raise (Internal_error ("LutProg.get_init_state",
("initial value of \""^nme^"\" must be a constant expression")
("initial value of \""^nme^"\" must be a constant expression"
^" (but get "^(Exp.to_string e)^")"
)
)) in
Value.OfIdent.add accin (nme, v)
)
......
......@@ -199,6 +199,7 @@ Utils.time_C "main_loop1";
) ^ "\n"
in
Rif.write stdout step_str;
Rif.flush stdout;
(* IF BOOT -> don't ask for input *)
let input =
if boot then Value.OfIdent.empty
......@@ -280,20 +281,95 @@ Utils.time_R "main_loop";
)
)
let dbgexe = Verbose.get_flag "LutExe"
(* simu with LutExe *)
let to_exe infile mnode = (
let exe = LutExe.make ~libs:(MainArg.libs()) infile mnode in
let ctrl = LutExe.get_init_state exe in
assert false
Verbose.exe ~flag:dbgexe (fun _ -> LutExe.dump exe);
let in_vars = LutExe.in_var_list exe in
let out_vars = LutExe.out_var_list exe in
let loc_vars = LutExe.loc_var_list exe in
let do_stop = match MainArg.max_steps () with
| None -> fun _ -> false
| Some max -> fun c -> (c <= max)
in
let rec do_step cpt ctrl ins pres = (
Verbose.put "#Main.to_exe: step %d\n" cpt;
let bg = LutExe.get_behavior_gen exe ins pres ctrl in
match bg () with
| LutExe.NoMoreBehavior -> (
Rif.write stdout "# Simulation ended with uncaught Deadlock\n";
Rif.flush stdout;
exit 2
)
| LutExe.SomeBehavior (b, bg') -> (
match b with
| LutExe.Goto (zeguard, ctrl') -> (
(* THIS IS THE NORMAL BEHAVIOR *)
let (outs, locs) = try
LutExe.find_one_sol exe zeguard