diff --git a/configure.ac b/configure.ac
index 0b8e4a2eea1da35ae9494312b0cb3de227655acb..20aa04550dcd5fc8b45d2d1fa730f7fe4f4a3115 100644
--- a/configure.ac
+++ b/configure.ac
@@ -78,12 +78,21 @@ AS_IF([ocamlfind query yojson >/dev/null 2>&1],
# Seal
AC_MSG_CHECKING(seal library (optional))
-AS_IF([ocamlfind query seal >/dev/null 2>&1; echo 1],
+AS_IF([ocamlfind query seal >/dev/null 2>&1],
[seal=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
)
AS_IF([test "x$seal" = "xyes"], [
AC_SUBST(LUSTREV_SEAL, "(module Seal_verifier.Verifier : VerifierType.S);")
- AC_SUBST(LUSTREV_SEAL_TAG, "") # <**/*>: package(seal)")
+ AC_SUBST(LUSTREV_SEAL_TAG, "<**/*>: package(seal)")
+])
+
+# Tiny
+AC_MSG_CHECKING(tiny library (optional))
+AS_IF([ocamlfind query tiny >/dev/null 2>&1],
+ [tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)],
+)
+AS_IF([test "x$tiny" = "xyes"], [
+ dnl AC_SUBST(LUSTREV_TINY_TAG, "<**/*>: package(apron.boxMPQ), package(apron.octMPQ), package(apron.polkaMPQ), package(tiny)")
])
# z3 (optional)
@@ -125,14 +134,14 @@ AS_IF([test "x$enable_z3" != "xno"], [
])
-# Tiny
-AC_MSG_CHECKING(tiny library (optional))
-AS_IF([ocamlfind query tiny >/dev/null 2>&1],
- [tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)],
-)
+dnl # Tiny
+dnl AC_MSG_CHECKING(tiny library (optional))
+dnl AS_IF([ocamlfind query tiny >/dev/null 2>&1],
+dnl [tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)],
+dnl )
AS_IF([test "x$tiny" = "xyes"], [
AC_SUBST(LUSTREV_TINY, "(module Tiny_verifier.Verifier : VerifierType.S);")
- AC_SUBST(LUSTREV_TINY_TAG, "<**/*>: package(tiny)")
+ AC_SUBST(LUSTREV_TINY_TAG, ["<**/*>: package(apron.boxMPQ), package(apron.octMPQ), package(apron.polkaMPQ), package(tiny)"])
])
# Salsa
diff --git a/src/_tags.in b/src/_tags.in
index 99a2f0e0b8da19dde34c595ce2d23dd662ed154e..00804196b20722bdc0a2088e22602776b73448a3 100644
--- a/src/_tags.in
+++ b/src/_tags.in
@@ -25,6 +25,7 @@ true: bin_annot, color(always)
"tools/stateflow/json-parser": include
"tools/importer": include
"tools/seal": include
+"tools/tiny": include
# svn
<**/.svn>: -traverse
@@ -36,11 +37,12 @@ true: bin_annot, color(always)
<**/*verifier.native> or <**/*.ml{,i}> : package(yojson)
<**/*.native> : use_str
-<**/main_lustre_compiler.native>: use_unix
-<**/main_lustre_testgen.native> : use_unix
-<**/main_lustre_verifier.native> : use_unix
-<**/sf_sem.native> : use_unix
+<**/main_lustre_compiler.native>: package(unix)
+<**/main_lustre_testgen.native> : package(unix)
+<**/main_lustre_verifier.native> : package(unix)
+<**/sf_sem.native> : package(unix)
<**/*> : package(num)
+<**/*> : package(zarith)
<**/*.ml> : package(logs)
<**/*.native> : package(logs)
<**/json_parser.ml> : package(yojson)
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 462de54dd05a246e2a4677231526db488b550017..3254d8ebc60c52b527b2318fb3727fb730d0bbe4 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -14,7 +14,7 @@ open Lustre_types
open Corelang
open Machine_code_types
(*open Machine_code_common*)
-
+module Mpfr = Lustrec_mpfr
let print_version fmt =
Format.fprintf fmt
diff --git a/src/compiler_stages.ml b/src/compiler_stages.ml
index 5011f12b3d4723a0889e90e6bffaabbf2f39d699..d1efba16f3fc56805186e0bfd8b691c492d424a8 100644
--- a/src/compiler_stages.ml
+++ b/src/compiler_stages.ml
@@ -2,6 +2,7 @@ open Format
open Utils
open Compiler_common
open Lustre_types
+module Mpfr = Lustrec_mpfr
exception StopPhase1 of program_t
diff --git a/src/machine_code_common.mli b/src/machine_code_common.mli
index 14584cace6bc299521be2c647d47dd20723e07cc..bf442400ab1eaffc4d8091a4f324c8857dfcd519 100644
--- a/src/machine_code_common.mli
+++ b/src/machine_code_common.mli
@@ -22,3 +22,4 @@ val get_machine: Machine_code_types.machine_t list -> string -> Machine_code_typ
val get_node_def: string -> Machine_code_types.machine_t -> Lustre_types.node_desc
val join_guards_list: Machine_code_types.instr_t list -> Machine_code_types.instr_t list
+val machine_vars: Machine_code_types.machine_t -> Lustre_types.var_decl list
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index a7391ee2511d61cbf99fb470747bd63f6beff79d..0e7bc0feeca67d6fa1794d5f2cc175015f92e2e7 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -52,7 +52,7 @@ let rec compile dirname basename extension =
if !Options.mpfr &&
extension = ".lus" (* trying to avoid the injection of the module for lusi files *)
then
- Mpfr.mpfr_module::prog
+ Lustrec_mpfr.mpfr_module::prog
else
prog
in
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 08eaddce8c6b4051e93b62e8a2959c398d0729a1..81eb797843941802dad5c37e8006284f29872d9a 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -16,6 +16,7 @@ open Corelang
open Causality
open Machine_code_common
open Dimension
+module Mpfr = Lustrec_mpfr
let pp_elim m fmt elim =
diff --git a/src/plugins/mpfr/mpfr.ml b/src/plugins/mpfr/lustrec_mpfr.ml
similarity index 100%
rename from src/plugins/mpfr/mpfr.ml
rename to src/plugins/mpfr/lustrec_mpfr.ml
diff --git a/src/real.ml b/src/real.ml
index 25954b69f3cbf2e616a2aeb3e4a1bd06d5aaf06f..3590fefad79e8e3ae074cb92fbe1250a3d804283 100644
--- a/src/real.ml
+++ b/src/real.ml
@@ -16,6 +16,16 @@ let to_num (c, e, s) =
let num_10 = Num.num_of_int 10 in
Num.(c // (num_10 **/ (num_of_int e)))
+let rec to_q (c, e, s) =
+ if e = 0 then
+ Q.of_string (Num.string_of_num c)
+ else
+ if e > 0 then Q.div (to_q (c,e-1,s)) (Q.of_int 10)
+ else (* if exp<0 then *)
+ Q.mul
+ (to_q (c,e+1,s))
+ (Q.of_int 10)
+
let to_string (_, _, s) = s
let eq r1 r2 =
diff --git a/src/real.mli b/src/real.mli
index 6787dcd88b174d254ac1e1fe3c488088730eefc5..fc3ce97b818f1c374dbf6b580d605876123d68ba 100644
--- a/src/real.mli
+++ b/src/real.mli
@@ -18,6 +18,7 @@ val eq: t -> t -> bool
val diseq: t -> t -> bool
val to_num: t -> Num.num
+val to_q: t -> Q.t
val to_string: t -> string
val eq: t -> t -> bool
val zero: t
diff --git a/src/tools/tiny/tiny_utils.ml b/src/tools/tiny/tiny_utils.ml
new file mode 100644
index 0000000000000000000000000000000000000000..57d6cb10b704832cbe2f30b14f521479986cd7ba
--- /dev/null
+++ b/src/tools/tiny/tiny_utils.ml
@@ -0,0 +1,211 @@
+
+module Ast = Tiny.Ast
+
+
+let lloc_to_tloc loc = Tiny.Location.dummy (*TODO*)
+
+let tloc_to_lloc loc = Location.dummy_loc (*TODO*)
+
+
+let ltyp_to_ttyp t =
+ if Types.is_real_type t then Tiny.Ast.RealT
+ else if Types.is_int_type t then Tiny.Ast.IntT
+ else if Types.is_bool_type t then Tiny.Ast.BoolT
+ else assert false (* not covered yet *)
+
+let cst_bool loc b =
+ { Ast.expr_desc =
+ if b then
+ Ast.Cst(Q.of_int 1, "true")
+ else
+ Ast.Cst(Q.of_int 0, "false");
+ expr_loc = loc;
+ expr_type = Ast.BoolT }
+
+let rec real_to_q man exp =
+ if exp = 0 then
+ Q.of_string (Num.string_of_num man)
+ else
+ if exp > 0 then Q.div (real_to_q man (exp-1)) (Q.of_int 10)
+ else (* if exp<0 then *)
+ Q.mul
+ (real_to_q man (exp+1))
+ (Q.of_int 10)
+
+let instr_loc i =
+ match i.Machine_code_types.lustre_eq with
+ | None -> Tiny.Location.dummy
+ | Some eq -> lloc_to_tloc eq.eq_loc
+
+let rec lval_to_texpr loc _val =
+ let build d v =
+ Ast.{ expr_desc = d;
+ expr_loc = loc;
+ expr_type = v }
+ in
+ let new_desc =
+ match _val.Machine_code_types.value_desc with
+ | Machine_code_types.Cst cst -> (
+ match cst with
+ Lustre_types.Const_int n -> Ast.Cst (Q.of_int n, string_of_int n)
+ | Const_real r -> Ast.Cst (Real.to_q r, Real.to_string r)
+ | _ -> assert false
+ )
+
+ | Var v -> Ast.Var (v.var_id)
+ | Fun (op, vl) ->
+ let t_arg = match vl with
+ | hd::_ -> ltyp_to_ttyp hd.value_type
+ | _ -> assert false
+ in
+ (
+ match op, List.map (lval_to_texpr loc) vl with
+ | "+", [v1;v2] -> Ast.Binop (Ast.Plus, v1, v2)
+ | "-", [v1;v2] -> Ast.Binop (Ast.Minus, v1, v2)
+ | "*", [v1;v2] -> Ast.Binop (Ast.Times, v1, v2)
+ | "/", [v1;v2] -> Ast.Binop (Ast.Div, v1, v2)
+ | "<", [v1;v2] ->
+ Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Strict)
+ | "<=", [v1;v2] ->
+ Ast.Cond (build(Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Loose)
+ | ">", [v1;v2] ->
+ Ast.Cond (build(Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Strict)
+ | ">=", [v1;v2] ->
+ Ast.Cond (build (Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Loose)
+ | "=", [v1;v2] ->
+ Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Zero)
+ | "!=", [v1;v2] ->
+ Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.NonZero)
+ | _ -> Format.eprintf "No tiny translation for operator %s@.@?" op; assert false
+ )
+ | _ -> assert false (* no array. access or power *)
+ in
+ build new_desc (ltyp_to_ttyp _val.value_type)
+
+
+let machine_body_to_ast init m =
+ let init_var = ref None in
+ let rec guarded_expr_to_stm loc te guarded_instrs =
+ match guarded_instrs with
+ | [] -> assert false
+ | [_,il] -> instrl_to_stm il
+ | (label, il)::tl ->
+ let stmt = instrl_to_stm il in
+ let guard= match label with
+ "true" -> te
+ | "false" -> Ast.neg_guard te
+ | _ -> assert false (* TODO: don't deal with non boolean
+ guards. Could just treturn true and
+ over-approximate behavior *)
+ in
+ if (match !init_var, te.Ast.expr_desc with
+ | Some v, Var v2 -> v = v2
+ | _ -> false) then
+ instrl_to_stm (
+ if init then
+ (List.assoc "true" guarded_instrs)
+ else
+ (List.assoc "false" guarded_instrs)
+ )
+ else
+ Ast.Ite (loc, guard, stmt, guarded_expr_to_stm loc te tl)
+ and instr_to_stm i =
+ let loc = instr_loc i in
+ match i.instr_desc with
+ | MLocalAssign (v, e) | MStateAssign (v, e) ->
+ Ast.Asn (loc, v.var_id, (lval_to_texpr loc) e)
+ | MBranch (e, guarded_instrs) -> (
+ let te = lval_to_texpr loc e in
+ guarded_expr_to_stm loc te guarded_instrs
+ )
+ | MStep (ol, id, args) ->
+ if List.mem_assoc id m.Machine_code_types.minstances then
+ let fun_name, _ = List.assoc id m.minstances in
+ match Corelang.node_name fun_name, ol with
+ | "_arrow", [o] -> (
+ init_var := Some o.var_id;
+ Ast.Nop (loc);
+ (* Ast.Asn (loc, o.var_id,
+ * { expr_desc = if init then Ast.Cst(Q.of_int 1, "true") else Ast.Cst(Q.of_int 0, "false");
+ * expr_loc = loc;
+ * expr_type = Ast.BoolT }
+ * ) *)
+ )
+ | name, _ ->
+ (
+ Format.eprintf "No tiny translation for node call %s@.@?" name;
+ assert false
+ )
+ else (
+ Format.eprintf "No tiny translation for node call %s@.@?" id;
+ assert false
+ )
+ | MReset id
+ | MNoReset id -> assert false (* no more calls or functions, ie. no reset *)
+ | MComment s
+ | MSpec s -> assert false
+ and instrl_to_stm il =
+ match il with
+ [] -> assert false
+ | [i] -> instr_to_stm i
+ | i::il ->
+ let i' = instr_to_stm i in
+ Ast.Seq (instr_loc i, i', (instrl_to_stm il))
+ in
+ instrl_to_stm m.Machine_code_types.mstep.step_instrs
+
+let read_var loc bounds_opt v =
+ let min, max =
+ match bounds_opt with
+ Some (min,max) -> min, max
+ | None -> (Q.of_int (-1), "-1"), (Q.of_int 1, "1")
+ in
+ let range = {
+ Ast.expr_desc = Ast.Rand (min,max);
+ expr_loc = loc;
+ expr_type = ltyp_to_ttyp (v.Lustre_types.var_type)
+ }
+ in
+ Ast.Asn (loc, v.var_id, range)
+
+let rec read_vars loc bounds_inputs vl =
+ match vl with
+ [] -> Ast.Nop loc
+ | [v] -> read_var
+ loc
+ (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
+ Some (List.assoc v.Lustre_types.var_id bounds_inputs)
+ else
+ None)
+ v
+ | v::tl ->
+ Ast.Seq (loc,
+ read_var
+ loc
+ (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
+ Some (List.assoc v.Lustre_types.var_id bounds_inputs)
+ else
+ None)
+ v,
+ read_vars loc bounds_inputs tl
+ )
+
+let machine_to_ast bounds_input m =
+ let loc = Tiny.Location.dummy in
+ let read_vars = read_vars loc bounds_input m.Machine_code_types.mstep.step_inputs in
+ let ast_loop_first = machine_body_to_ast true m in
+ let ast_loop_run = machine_body_to_ast false m in
+ let ast_loop_body = Ast.Seq (loc, read_vars, ast_loop_run) in
+ let loop = Ast.While(loc, cst_bool loc true, ast_loop_body) in
+ Ast.Seq (loc, read_vars, (Ast.Seq (loc, ast_loop_first, loop)))
+
+let machine_to_env m =
+
+ List.fold_left (fun accu v ->
+ let typ =
+ ltyp_to_ttyp (v.Lustre_types.var_type)
+ in
+ Ast.VarSet.add (v.var_id, typ) accu)
+ Ast.VarSet.empty
+ (Machine_code_common.machine_vars m)
+
diff --git a/src/tools/tiny/tiny_verifier.ml b/src/tools/tiny/tiny_verifier.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2531f58f36c5c89bee7c87215db358512e981c15
--- /dev/null
+++ b/src/tools/tiny/tiny_verifier.ml
@@ -0,0 +1,66 @@
+
+let active = ref false
+let tiny_debug = ref false
+
+
+let tiny_run ~basename prog machines =
+ let node_name =
+ match !Options.main_node with
+ | "" -> (
+ Format.eprintf "Tiny verifier requires a main node.@.";
+ Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
+ (Utils.fprintf_list ~sep:"@ "
+ (fun fmt m ->
+ Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id
+ )
+ )
+ machines;
+ exit 1
+ )
+ | s -> ( (* should have been addessed before *)
+ match Machine_code_common.get_machine_opt machines s with
+ | None -> begin
+ Global.main_node := s;
+ Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
+ raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
+ end
+ | Some _ -> s
+ )
+ in
+ let m = Machine_code_common.get_machine machines node_name in
+ let env = (* We add each variables of the node the Tiny env *)
+ Tiny_utils.machine_to_env m in
+ let nd = m.mname in
+ (* Building preamble with some bounds on inputs *)
+ (* TODO: deal woth contracts, asserts, ... *)
+ let bounds_inputs = [] in
+ let ast = Tiny_utils.machine_to_ast bounds_inputs m in
+ let mems = m.mmemory in
+
+ Format.printf "%a@." Tiny.Ast.fprint_stm ast;
+
+ ()
+
+
+module Verifier =
+ (struct
+ include VerifierType.Default
+ let name = "tiny"
+ let options =
+ [
+ "-debug", Arg.Set tiny_debug, "tiny debug"
+ ]
+
+ let activate () =
+ active := true;
+ (* Options.global_inline := true;
+ * Options.optimization := 0;
+ * Options.const_unfold := true; *)
+ ()
+
+ let is_active () = !active
+ let run = tiny_run
+
+
+ end: VerifierType.S)
+