Commit 31b88b58 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Fix a Makefile subtle bug.

Indeed, in source/Lutin/Makefile.lut4ocaml, I was including
rdbg-plugin when building the lut4ocaml.cma/cmxa lib. The consequence
was that the OcamlRM module was included twice, with its local
Hashtbl (used for registering/loading Dynlink stuff) duplicated!

Dynlink is to be used with great care !!!

Also reflect the changes in the rdbg-plugin
- in the OcamlRM module (s/add_/reg_/g)
- in the Event module (more field of src_info type)
cf rdbg git version 142783a77cad1a0f7ef91972b8376f0b0e44b878

also mv lut_evt stuff from LutinRun to rdbg (in LutinRdbg module).
parent 3721d420
(**************************************************************************)
(* Utilities *)
......@@ -153,10 +152,10 @@ let (step : Data.subst list -> Data.subst list)=
bounds
let _ =
OcamlRM.add_inputs "rabbit.cmxs" inputs;
OcamlRM.add_outputs "rabbit.cmxs" outputs;
OcamlRM.add_kill "rabbit.cmxs" kill;
OcamlRM.add_step "rabbit.cmxs" step;
OcamlRM.add_mems "rabbit.cmxs" mems_i mems_o
OcamlRM.reg_inputs "rabbit.cmxs" inputs;
OcamlRM.reg_outputs "rabbit.cmxs" outputs;
OcamlRM.reg_kill "rabbit.cmxs" kill;
OcamlRM.reg_step "rabbit.cmxs" step;
OcamlRM.reg_mems "rabbit.cmxs" mems_i mems_o
......@@ -145,8 +145,6 @@ LTOP_SOURCES = \
$(OBJDIR)/lus2licRun.ml \
$(OBJDIR)/lutinRun.mli \
$(OBJDIR)/lutinRun.ml \
$(OBJDIR)/ocamlRun.mli \
$(OBJDIR)/ocamlRun.ml \
$(OBJDIR)/lustreRun.mli \
$(OBJDIR)/lustreRun.ml \
$(OBJDIR)/ocaml.mli \
......
......@@ -51,15 +51,12 @@ let (collect : bool -> Bdd.t -> Expr.t) =
let lminus l1 l2 = List.filter (fun x -> not (List.mem x l2)) l1
(* exported *)
let (get_info : Bdd.t -> Bdd.t -> (Expr.t * Bdd.t) -> Failure.info) =
let (get_info : Bdd.t -> Bdd.t -> (Expr.t * Bdd.t) -> Expr.t) =
fun bdd bdd1 (expr2,bdd2) ->
assert (not(Bdd.is_false bdd1));
let is_sat = not (Bdd.is_false bdd) in
if is_sat then
Failure.Numeric (collect true bdd)
else if Bdd.is_false bdd2 then
Failure.Boolean expr2
else
if is_sat then collect true bdd
else if Bdd.is_false bdd2 then expr2 else
(* try to simplify the formula associated to bdd by projet *)
let s1 = Bdd.list_of_support (Bdd.support bdd1)
and s2 = Bdd.list_of_support (Bdd.support bdd2) in
......@@ -70,6 +67,6 @@ let (get_info : Bdd.t -> Bdd.t -> (Expr.t * Bdd.t) -> Failure.info) =
assert (not(Bdd.is_false bdd1));
assert (not(Bdd.is_false bdd2));
assert (Bdd.is_false (Bdd.dand bdd1 bdd2));
Failure.Boolean (Expr.Op(Expr.And, [collect false bdd1; collect false bdd2]))
Expr.Op(Expr.And, [collect false bdd1; collect false bdd2])
(* Try to explain why a constraint is not satisfiable. It can be due
to:
(* Try to explain why a constraint is not satisfiable by providing a smaller
sub-expression of the expression encoded in the bdd.
Such an expressions can be unsatisfiable for :
- a pure Boolean reason, in which case we provide a (minimal)
expression representing the list of monomes that makes it false);
......@@ -17,4 +19,4 @@
- bdd=bdd1^bdd2 has no sol
- bdd2=to_bdd(e2).
*)
val get_info : Bdd.t -> Bdd.t -> (Expr.t * Bdd.t) -> Failure.info
val get_info : Bdd.t -> Bdd.t -> (Expr.t * Bdd.t) -> Expr.t
......@@ -26,7 +26,7 @@ endif
OCAMLFLAGS += -I +rdbg-plugin
OCAMLLDFLAGS += -I +rdbg-plugin
LIBS = unix str nums polka bdd rdbg-plugin
LIBS = unix str nums polka bdd
CLIBS = bdd_stubs camlidl
CLIBS = bdd_stubs bdd camlidl gmp stdc++ polkag_caml polkag
......
(* Time-stamp: <modified the 17/12/2013 (at 11:03) by Erwan Jahier> *)
(* Time-stamp: <modified the 21/02/2014 (at 16:02) by Erwan Jahier> *)
(* generate ocaml glue code that makes it possible to call lutin
from ocaml with the current set of arguments.
......@@ -34,10 +34,10 @@ any ocaml programs (as rdbg does).
*)
let dyn_file = (Dynlink.adapt_filename \"%s\")
let _ =
OcamlRM.add_inputs dyn_file inputs;
OcamlRM.add_outputs dyn_file outputs;
OcamlRM.add_kill dyn_file kill;
OcamlRM.add_step dyn_file step;
OcamlRM.add_step_dbg dyn_file step_dbg;
OcamlRM.add_mems dyn_file mems_i mems_o
OcamlRM.reg_inputs dyn_file inputs;
OcamlRM.reg_outputs dyn_file outputs;
OcamlRM.reg_kill dyn_file kill;
OcamlRM.reg_step dyn_file step;
OcamlRM.reg_step_dbg dyn_file step_dbg;
OcamlRM.reg_mems dyn_file mems_i mems_o
" entete args_str cma_file
......@@ -782,3 +782,5 @@ lutin-labo-install:
cp -f $(OBJDIR)/*Ezdl_c_stubs* $(CAML_INSTALL_DIR)/lutin
cp ../working/$(HOSTTYPE)/lib/* $(CAML_INSTALL_DIR)/lutin
labo: lutin-labo-install
(* Time-stamp: <modified the 20/02/2014 (at 10:26) by Erwan Jahier> *)
(* Time-stamp: <modified the 24/02/2014 (at 10:41) by Erwan Jahier> *)
(**********************************************************************************)
type vars = (string * Data.t) list
......@@ -96,34 +96,5 @@ let make_lut argv =
lut_in, lut_out, (fun _ -> ()), lut_step, lut_step_dbg, mems_in, mems_out
type lut_evt =
| Ltop | Call | Exit
| Try (* Try a constraint to compute the current step *)
| Sat (* the tryied constraint is Satisfiable *)
| Nsat (* the tryied constraint is Not satisfiable *)
(* | Deadlock *)
(*
(Ltop (Call (Try.Nsat*.Sat))* Exit)* )*
*)
let (to_lut_evt: Event.kind -> lut_evt) = function
| Event.Ltop -> Ltop
| Event.Call -> Call
| Event.Exit -> Exit
(* | Event.Abort -> Deadlock *)
| Event.MicroStep "try " -> Try
| Event.MicroStep "sat " -> Sat
| Event.MicroStep "usat" -> Nsat
| Event.MicroStep _ -> assert false
let (from_lut_evt: lut_evt -> Event.kind) = function
| Ltop -> Event.Ltop
| Call -> Event.Call
| Exit -> Event.Exit
| Try -> Event.MicroStep "try "
| Sat -> Event.MicroStep "sat "
| Nsat -> Event.MicroStep "usat"
(* | Deadlock -> Event.Abort *)
(* Time-stamp: <modified the 19/02/2014 (at 17:56) by Erwan Jahier> *)
(* Time-stamp: <modified the 24/02/2014 (at 10:40) by Erwan Jahier> *)
type vars = (string * Data.t) list
......@@ -9,13 +9,3 @@ val make_lut: string array ->
* Data.subst list * Data.subst list
type lut_evt =
| Ltop | Call | Exit
| Try (* Try a constraint to compute the current step *)
| Sat (* the tryied constraint is Satisfiable *)
| Nsat (* the tryied constraint is Not satisfiable *)
(* | Deadlock *)
val to_lut_evt: Event.kind -> lut_evt
val from_lut_evt: lut_evt -> Event.kind
(* Time-stamp: <modified the 19/02/2014 (at 15:35) by Erwan Jahier> *)
(* class type ocaml_reactive_machine = *)
(* object *)
(* method step : Data.subst list -> Data.subst list *)
(* method kill : string -> unit *)
(* end;; *)
type vars = (Data.ident * Data.t) list
let (make_ocaml : string -> vars * vars *
(string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) *
Data.subst list * Data.subst list) =
fun cmxs ->
let _ =
try Dynlink.loadfile cmxs
with Dynlink.Error msg ->
Printf.eprintf "\n*** error in rdbg (Dynlink.loadfile %s).\n*** %s.\n"
cmxs (Dynlink.error_message msg);
flush stderr;
exit 2
in
let imems, omems = OcamlRM.get_mems cmxs in
let inputs = OcamlRM.get_inputs cmxs in
let inputs = List.map (fun (n,t) -> n, t) inputs in
let outputs = OcamlRM.get_outputs cmxs in
let outputs = List.map (fun (n,t) -> n, t) outputs in
let step_dbg =
try OcamlRM.get_step_dbg cmxs
with _ ->
let step_dbg sl ctx cont =
{
Event.step = ctx.Event.ctx_step;
Event.data = ctx.Event.ctx_data;
Event.nb = Event.get_nb ();
Event.depth = ctx.Event.ctx_depth;
Event.kind = Event.Exit;
Event.name = cmxs;
Event.lang = "ocaml";
Event.inputs = inputs;
Event.outputs = outputs;
Event.sinfo = None;
Event.next = (fun () -> cont (OcamlRM.get_step cmxs sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
}
in
step_dbg
in
let res = (
inputs, outputs,
OcamlRM.get_kill cmxs,
OcamlRM.get_step cmxs,
step_dbg,
imems,
omems
)
in
Printf.eprintf "rdbg: %s file loaded.\n" cmxs;
res
(* cf
http://blog.rastageeks.org/ocaml/article/dynlink-as-dlopen
http://okmij.org/ftp/ML/first-class-modules/
*)
type vars = (Data.ident * Data.t) list
val make_ocaml : string -> vars * vars *
(string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
* Data.subst list * Data.subst list
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