Skip to content

GitLab

Commit c0c3ea3a authored by Erwan Jahier's avatar Erwan Jahier
Browse files

ldbg: attach a Event.exp to fail and exit ports that correspond to the constraint.

parent ecd6900d
Hide whitespace changes
Inline Side-by-side
examples/lutin/ldbg/test3.ml
View file @ c0c3ea3a
......@@ -100,8 +100,8 @@ del_hooks "print_event";;
let src =
match e.kind with
| Node {port=Exit(cstr,src)}
| Node {port=Fail(cstr,src)} ->
| Node {port=Exit(cstr,_,src)}
| Node {port=Fail(cstr,_,src)} ->
List.iter (fun si -> print_string si.str) (src());
| _ -> ()
;;
......
source/Lurettetop/event.ml
View file @ c0c3ea3a
......@@ -9,9 +9,22 @@ type ctx = (* herited debug info *)
ctx_outputs : string list;
}
(* Expressions *)
type exp =
| Op of oper * exp list
| True | False
| Ival of Num.num | Fval of float
| Var of string
and
oper =
| And | Or | Xor | Impl | Not | Eq | Ite
| Sup | SupEq | Inf | InfEq
| Sum | Diff | Prod | Quot | Mod | Div | Uminus
| Call of string
type src_info = {
str : string ;
str : string ;
file : string ;
line : int * int ;
char : int * int ;
......@@ -19,12 +32,22 @@ type src_info = {
}
(* Try to explain why a constraint is not satisfiable. It can be due
to a pure Boolean reason (in which case we provide xxx); Or there
do exist Boolean solution, but no numeric ones (in which case we
provide the list of monomes) *)
type failure_info =
| Boolean of exp list
| Numeric of exp list
(* Source info related to the elected constraint *)
type cstr_lazy_src_info = (unit -> src_info list)
type port =
| Call
| Exit of string (* The elected contraint that produced the outputs *) * cstr_lazy_src_info
| Fail of string (* The elected contraint that failed *) * cstr_lazy_src_info
| Exit of string * exp (* The elected contraint that produced the outputs *) * cstr_lazy_src_info
| Fail of string * exp (* The elected contraint that failed *) * cstr_lazy_src_info
(* * (unit -> failure_info) *)
type node_info = {
......@@ -74,3 +97,5 @@ let incr_nb() =
incr event_nb
source/Lurettetop/ldbg.ml
View file @ c0c3ea3a
......@@ -118,13 +118,13 @@ help \"command\";;
else if cmd="utils" then (
print_cmd_list cmd_list_utils
)
else if List.mem_assoc cmd cmd_list then (
let prof,help = List.assoc cmd cmd_list in
else if List.mem_assoc cmd all_cmds then (
let prof,help = List.assoc cmd all_cmds in
Printf.printf "%s : %s\n%s\n" cmd prof help
)
else (
Printf.printf "Unknown command. Available commands are : %s"
(String.concat "," (fst (List.split cmd_list)))
(String.concat "," (fst (List.split all_cmds)))
)
let h = help
......
source/Lurettetop/ldbg_utils.ml
View file @ c0c3ea3a
......@@ -30,23 +30,23 @@ let print_src_info si =
let (print_src : Event.t -> unit) =
fun e ->
match e.kind with
| Node { port = Exit(_,src) }
| Node { port = Fail(_,src) } ->
| Node { port = Exit(_,_,src) }
| Node { port = Fail(_,_,src) } ->
List.iter print_src_info (src())
|_ -> ();;
let (print_cstr : Event.t -> unit) =
fun e ->
match e.kind with
| Node { port = Exit(cstr,_) }
| Node { port = Fail(cstr,_) } ->
| Node { port = Exit(cstr,_,_) }
| Node { port = Fail(cstr,_,_) } ->
print_string (" \"" ^cstr ^ "\"")
|_ -> ();;
let (port2str: Event.port -> string) =
function
| Exit (_,_)-> "exit"
| Fail (_,_) -> "fail"
| Exit (_,_,_)-> "exit"
| Fail (_,_,_) -> "fail"
| Call -> "call"
let print_event (e:t) =
......@@ -138,8 +138,8 @@ let rec (next_line : Event.t -> string -> int -> Event.t) =
fun e f line ->
let the_line e =
match e.kind with
| Node { port = Exit(_,src)}
| Node { port = Fail(_,src)} ->
| Node { port = Exit(_,_,src)}
| Node { port = Fail(_,_,src)} ->
List.exists
(fun si ->
Filename.basename si.file = f &&
......@@ -169,8 +169,8 @@ let (break_matches : Event.t -> string -> bool) =
| (Ltop),_ -> false
| Node _, [] -> false
| Node { port = Call}, _ -> false
| Node { name=name; port = Fail(_,src)}, str::tail
| Node { name=name; port = Exit(_,src)}, str::tail ->
| Node { name=name; port = Fail(_,_,src)}, str::tail
| Node { name=name; port = Exit(_,_,src)}, str::tail ->
if Sys.file_exists str then
match tail with
| [ln] ->
......@@ -242,8 +242,8 @@ let incr_prof si =
let (prof_add: Event.t -> unit) =
fun e ->
match e.kind with
| Node { port = Exit(_,src) }
| Node { port = Fail(_,src) } ->
| Node { port = Exit(_,_,src) }
| Node { port = Fail(_,_,src) } ->
List.iter incr_prof (src())
| _ -> ()
......
source/Lutin/Makefile.lutin
View file @ c0c3ea3a
......@@ -46,6 +46,8 @@ SOURCES=$(LUTIN_SOURCES) \
RESULT=lutin$(EXE)
ln: $(OBJDIR) $(SOURCES)
xxx:
echo "OCAMLDEP=$(OCAMLDEP)"
all: ln
make $(COMPIL_MODE)
......
source/Lutin/coAlgExp.ml
View file @ c0c3ea3a
......@@ -195,3 +195,21 @@ let lus_dumps ae = (
Buffer.reset zebuff;
res
)
(*
let rec (to_event_exp : t -> Event.exp) =
fun ae ->
match ae.ae_val with
AE_true -> Event.True
| AE_false -> Event.False
| AE_const str -> Event.Const str
| AE_iconst i -> Event.Const i
| AE_rconst i -> Event.Const i
| AE_ival i -> Event.Ival i
| AE_rval r -> Event.Fval r
| AE_support s -> Event.var s
| AE_pre s -> pr "pre "; pr (CoIdent.to_string s)
| AE_alias s -> Event.var (CoIdent.to_string s)
| AE_external_call (s, _, _,args)
| AE_call (s, args) ->
*)
source/Lutin/lutExe.ml
View file @ c0c3ea3a
......@@ -420,46 +420,45 @@ let find_some_sols
| Some s -> s
| None ->
(* Formula_to_bdd.clear_step (); *)
(* !Solver.clear_snt (); *)
let zesol = (
(* Formula_to_bdd.clear_step (); *)
(* !Solver.clear_snt (); *)
let zesol = (
(* HERE : don't know exactly why but it seems to be
necessary to call Solver.is_satisfiable first
*)
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 *)
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 *)
(Verbose.level())
"LutExe.is_bool_sat" (* ctx_msg: string *)
g.g_form
"LutExe.is_bool_sat" (* msg: string (?) *)
in
if not is_bool_sat then (
[]
) else (
let sols = Solver.solve_formula
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
(Verbose.level())
"LutExe.is_bool_sat" (* ctx_msg: string *)
g.g_form
"LutExe.is_bool_sat" (* msg: string (?) *)
in
if not is_bool_sat then (
[]
) else (
let sols = Solver.solve_formula
Value.OfIdent.empty (* input: Var.env_in *)
Value.OfIdent.empty (* memory: Var.env *)
(* !solver_vl (* vl: int *) *)
(Verbose.level())
"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.g_form (* f: formula *)
in
sols
)
) in (
g.g_sol <- Some zesol;
zesol
)
(Verbose.level())
"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.g_form (* f: formula *)
in
sols
)
) in (
g.g_sol <- Some zesol;
zesol
)
let find_one_sol it g =
......@@ -518,27 +517,27 @@ let rec (to_src_info: CoIdent.src_stack -> Event.src_info) =
match l with
| [] -> raise No_src_info
| (lxm, _,None)::tl ->
{
Event.str = lxm.Lexeme.str;
Event.file = lxm.Lexeme.file;
Event.line = lxm.Lexeme.line, lxm.Lexeme.line;
Event.char = lxm.Lexeme.chstart, lxm.Lexeme.chend;
Event.stack = if tl=[] then None else Some (to_src_info tl);
}
{
Event.str = lxm.Lexeme.str;
Event.file = lxm.Lexeme.file;
Event.line = lxm.Lexeme.line, lxm.Lexeme.line;
Event.char = lxm.Lexeme.chstart, lxm.Lexeme.chend;
Event.stack = if tl=[] then None else Some (to_src_info tl);
}
| (lxm,_,Some ve)::tl ->
let line_b, line_e, char_b, char_e = cstr_src_info_of_val_exp ve in
let file = lxm.Lexeme.file in
let filecontent = Util.readfile file in
{
Event.str =
(try String.sub filecontent char_b (char_e - char_b + 1)
with _ ->
Printf.sprintf "%s: fail to get chars %i-%i" file char_b char_e);
Event.file = file;
Event.line = line_b, line_e;
Event.char = char_b, char_e;
Event.stack = if tl=[] then None else Some (to_src_info tl);
}
let line_b, line_e, char_b, char_e = cstr_src_info_of_val_exp ve in
let file = lxm.Lexeme.file in
let filecontent = Util.readfile file in
{
Event.str =
(try String.sub filecontent char_b (char_e - char_b + 1)
with _ ->
Printf.sprintf "%s: fail to get chars %i-%i" file char_b char_e);
Event.file = file;
Event.line = line_b, line_e;
Event.char = char_b, char_e;
Event.stack = if tl=[] then None else Some (to_src_info tl);
}
let add_to_guard_nc it data (e:CoAlgExp.t) (acc:guard) (si:CoTraceExp.src_info) =
......@@ -1478,12 +1477,11 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
let new_acc = add_to_guard_nc it data ae acc si in
if (check_satisfiablity it new_acc) then
br_cont.doit_ldbg (Goto (new_acc, TE_eps)) cont
else
else
let lazy_si () = List.map to_src_info (
if snd si = [] then acc.g_src else (snd si)::acc.g_src)
if snd si = [] then acc.g_src else (snd si)::acc.g_src)
in
let cstr = Exp.to_event_formula new_acc.g_form in
let event =
{
Event.step = ctx.Event.ctx_step;
......@@ -1494,7 +1492,7 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
{
Event.lang = "lutin";
Event.name = ctx.Event.ctx_name;
Event.port = Event.Fail (CoAlgExp.lus_dumps ae, lazy_si);
Event.port = Event.Fail (CoAlgExp.lus_dumps ae,cstr,lazy_si);
Event.inputs = ctx.Event.ctx_inputs;
Event.outputs = ctx.Event.ctx_outputs;
};
......@@ -2183,6 +2181,7 @@ and (to_reactive_prg_ldbg : Event.ctx -> string -> t -> internal_state -> Value.
in
let enb = Event.incr_nb (); Event.get_nb () in
let lazy_si () = List.map to_src_info zeguard.g_src in
let cstr = Exp.to_event_formula zeguard.g_form in
let event =
{
Event.step = ctx.Event.ctx_step;
......@@ -2192,7 +2191,7 @@ and (to_reactive_prg_ldbg : Event.ctx -> string -> t -> internal_state -> Value.
Event.Node
{
Event.lang = "lutin";
Event.port = Event.Exit (guard_to_string zeguard, lazy_si);
Event.port = Event.Exit (guard_to_string zeguard, cstr,lazy_si);
Event.name = rid;
Event.inputs = ctx.Event.ctx_inputs;
Event.outputs = ctx.Event.ctx_outputs;
......@@ -2368,6 +2367,7 @@ let (step_ldbg: Event.ctx -> string -> t -> control_state -> data_state ->
let edata = edata @ (get_sl (loc_var_list prog) locs) in
let enb = Event.incr_nb (); Event.get_nb () in
let lazy_si () = List.map to_src_info zeguard.g_src in
let cstr = Exp.to_event_formula zeguard.g_form in
{
Event.step = ctx.Event.ctx_step;
Event.nb = enb;
......@@ -2376,7 +2376,7 @@ let (step_ldbg: Event.ctx -> string -> t -> control_state -> data_state ->
Event.Node {
Event.lang = "lutin";
Event.name = node;
Event.port = Event.Exit (guard_to_string zeguard, lazy_si);
Event.port = Event.Exit (guard_to_string zeguard, cstr, lazy_si);
Event.inputs = ctx.Event.ctx_inputs;
Event.outputs = ctx.Event.ctx_outputs;
};
......
source/Makefile.release
View file @ c0c3ea3a
......@@ -6,7 +6,6 @@ ver:
echo version=$(VERSION)
strip:
strip ../$(HOSTTYPE)/bin/lucky$(EXE)
strip ../$(HOSTTYPE)/bin/lurettetop_exe$(EXE)
strip ../$(HOSTTYPE)/bin/xlurette_exe$(EXE) || true
strip ../$(HOSTTYPE)/bin/gen_stubs_exe$(EXE)
......@@ -251,7 +250,7 @@ test-lutin-rel:
#################################################################################################"
OCAMLC_RELEASE_NAME=$(shell ocamlc -v | grep version | cut -d " " -f6)
OCAMLC_RELEASE_NAME=$(shell ocamlc -version)
DRAW_RELEASE_NAME=luckyDraw_$(VERSION)_$(HOSTTYPE)+ocaml-$(OCAMLC_RELEASE_NAME)
draw-rel: $(DRAW_RELEASE_NAME).tgz
......
source/common/exp.ml
View file @ c0c3ea3a
......@@ -167,12 +167,9 @@ let _ = assert (
let _ = assert (
(remove_var_name "s[23].field[1]" = "[23].field[1]"))
(****************************************************************************)
let type_num_tbl = Hashtbl.create 100
(* exported *)
......@@ -416,3 +413,50 @@ let (weight_to_string : weight -> string) =
| Infinity -> ("Infinity")
(****************************************************************************)
let (to_event_formula : formula -> Event.exp) =
fun f ->
let op oper args = Event.Op(oper,args) in
let rec aux f = match f with
| And (f1, f2) -> op Event.And [aux f1; aux f2]
| Or (f1, f2) -> op Event.Or [aux f1; aux f2]
| Xor (f1, f2) -> op Event.Xor [aux f1; aux f2]
| Impl(f1, f2) -> op Event.Impl [aux f1; aux f2]
| IteB(c, f1, f2) -> op Event.Ite [aux c; aux f1; aux f2]
| Not (f) -> op Event.Not [aux f]
| EqB (f1, f2) -> op Event.Eq [aux f1; aux f2]
| True -> Event.True
| False -> Event.False
| Bvar var -> Event.Var (Var.name var)
| Eq (n1, n2) -> op Event.Eq [auxe n1; auxe n2]
| Sup (n1, n2) -> op Event.Sup [auxe n1; auxe n2]
| SupEq(n1, n2) -> op Event.SupEq [auxe n1; auxe n2]
| Inf (n1, n2) -> op Event.Inf [auxe n1; auxe n2]
| InfEq(n1, n2) -> op Event.InfEq [auxe n1; auxe n2]
and auxe e = match e with
| Sum (n1, n2) -> op Event.Sum [auxe n1; auxe n2]
| Diff(n1, n2) -> op Event.Diff [auxe n1; auxe n2]
| Prod(n1, n2) -> op Event.Prod [auxe n1; auxe n2]
| Quot(n1, n2) -> op Event.Quot [auxe n1; auxe n2]
| Mod (n1, n2) -> op Event.Mod [auxe n1; auxe n2]
| Div (n1, n2) -> op Event.Div [auxe n1; auxe n2]
| Uminus(num) -> op Event.Uminus [auxe num]
| Ival(i) -> Event.Ival i
| Fval(f) -> Event.Fval f
| Ivar(var) -> Event.Var (Var.name var)
| Fvar(var) -> Event.Var (Var.name var)
| Ite(f, n1, n2) -> op Event.Ite [aux f; auxe n1; auxe n2]
| Inf_int -> assert false
| FFC(func_call_arg) -> assert false
| IFC(func_call_arg) -> assert false
| Gcont(n1, n2, num) -> assert false
| Gstop(n1, n2, num) -> assert false
| Icont(n1, n2, num) -> assert false
| Istop(n1, n2, num) -> assert false
in
aux f
source/common/exp.mli
View file @ c0c3ea3a
......@@ -151,3 +151,5 @@ val print_var : var -> unit
val remove_var_name : string -> string
val simplifie_a_little : formula -> formula
(****************************************************************************)
val to_event_formula : formula -> Event.exp
source/common/formula_to_bdd.ml
View file @ c0c3ea3a
......@@ -791,3 +791,5 @@ and
gne
((Bdd.dfalse !bdd_manager), false)
)
(***********************************************************************)
source/common/lustreRun.ml
View file @ c0c3ea3a
......@@ -95,7 +95,7 @@ let (make_ec : string -> vars * vars * (string -> unit) *
Event.kind = Event.Node
{
Event.lang = "lustre";
Event.port = Event.Exit("",fun () -> []);
Event.port = Event.Exit("",Event.True,fun () -> []);
Event.name=ec_file;
Event.inputs = [] ;
Event.outputs = [];
......@@ -219,7 +219,7 @@ let (make_socket_do : string -> int -> in_channel *
{
Event.lang = "socket";
Event.name=sock_adr ^ ":" ^ (string_of_int port);
Event.port = Event.Exit("",fun () -> []);
Event.port = Event.Exit("",Event.True,fun () -> []);
Event.inputs = [] ;
Event.outputs = [];
......@@ -322,7 +322,7 @@ let (make_ec_exe : string -> vars * vars * (string -> unit) *
{
Event.lang = "ec";
Event.name=ec_file;
Event.port = Event.Exit("",fun() -> []);
Event.port = Event.Exit("",Event.True,fun() -> []);
Event.inputs = [] ;
Event.outputs = [];
......@@ -506,7 +506,7 @@ let (make_ocaml : string -> vars * vars *
{
Event.lang = "ocaml";
Event.name=cmxs;
Event.port = Event.Exit("",fun() -> []);
Event.port = Event.Exit("",Event.True,fun() -> []);
Event.inputs = [] ;
Event.outputs = [];
......
source/common/polyhedron.ml
View file @ c0c3ea3a
......@@ -90,6 +90,9 @@ let number_of_ending_zero str =
l - (aux str l)
(* We need to translaste expressions into a string of the format used
by Polka to parse constraints *)
let rec (ineq_to_polka_string : Constraint.ineq -> string) =
......@@ -146,6 +149,8 @@ and
in
sign ^ numerator ^ "/" ^ denom
in
(* Printf.eprintf "Converting %f into the rat %s\n" f res; *)
(* flush stderr; *)
res
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment