Skip to content
Snippets Groups Projects
Commit f0195e96 authored by Pierre Loic Garoche's avatar Pierre Loic Garoche
Browse files

- Primitive Tiny backend

- Renamed Mpfr to lustrec_mpfr
- Introduced dependency in Zarith. Trying to move away from Num
parent 2120af73
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
......@@ -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)
......
......@@ -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
......
......@@ -2,6 +2,7 @@ open Format
open Utils
open Compiler_common
open Lustre_types
module Mpfr = Lustrec_mpfr
exception StopPhase1 of program_t
......
......@@ -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
......@@ -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
......
......@@ -16,6 +16,7 @@ open Corelang
open Causality
open Machine_code_common
open Dimension
module Mpfr = Lustrec_mpfr
let pp_elim m fmt elim =
......
File moved
......@@ -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 =
......
......@@ -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
......
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)
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)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment