CristalCaveGem » LustreC

AS_IF([ocamlfind query seal >/dev/null 2>&1],

   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)")

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 )

   AC_SUBST(LUSTREV_TINY_TAG, ["<**/*>: package(apron.boxMPQ), package(apron.octMPQ), package(apron.polkaMPQ), package(tiny)"])

"tools/tiny": include

<**/main_lustre_compiler.native>: package(unix)

<**/main_lustre_testgen.native> : package(unix)

<**/main_lustre_verifier.native> : package(unix)

<**/sf_sem.native>              : package(unix)

<**/*>                          : package(zarith)

module Mpfr = Lustrec_mpfr

module Mpfr = Lustrec_mpfr

val machine_vars: Machine_code_types.machine_t -> Lustre_types.var_decl list

      Lustrec_mpfr.mpfr_module::prog

module Mpfr = Lustrec_mpfr

(********************************************************************)

(*                                                                  *)

(*  The LustreC compiler toolset   /  The LustreC Development Team  *)

(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)

(*                                                                  *)

(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)

(*  under the terms of the GNU Lesser General Public License        *)

(*  version 2.1.                                                    *)

(*                                                                  *)

(********************************************************************)

open Utils

open Lustre_types

open Machine_code_types

open Corelang

open Normalization

open Machine_code_common

let report = Log.report ~plugin:"MPFR"

let mpfr_module = mktop (Open(false, "mpfr_lustre"))

let cpt_fresh = ref 0

let mpfr_rnd () = "MPFR_RNDN"

let mpfr_prec () = !Options.mpfr_prec

let inject_id = "MPFRId"

let inject_copy_id = "mpfr_set"

let inject_real_id = "mpfr_set_flt"

let inject_init_id = "mpfr_init2"

let inject_clear_id = "mpfr_clear"

let mpfr_t = "mpfr_t"

let unfoldable_value value =

  not (Types.is_real_type value.value_type && is_const_value value)

let inject_id_id expr =

  let e = mkpredef_call expr.expr_loc inject_id [expr] in

  { e with

    expr_type = Type_predef.type_real;

    expr_clock = expr.expr_clock;

  }

let pp_inject_real pp_var pp_val fmt var value =

  Format.fprintf fmt "%s(%a, %a, %s);"

    inject_real_id

    pp_var var

    pp_val value

    (mpfr_rnd ())

let inject_assign expr =

  let e = mkpredef_call expr.expr_loc inject_copy_id [expr] in

  { e with

    expr_type = Type_predef.type_real;

    expr_clock = expr.expr_clock;

  }

let pp_inject_copy pp_var fmt var value =

  Format.fprintf fmt "%s(%a, %a, %s);"

    inject_copy_id

    pp_var var

    pp_var value

    (mpfr_rnd ())

let rec pp_inject_assign pp_var fmt var value =

  if is_const_value value

  then

    pp_inject_real pp_var pp_var fmt var value

  else

    pp_inject_copy pp_var fmt var value

let pp_inject_init pp_var fmt var =

  Format.fprintf fmt "%s(%a, %i);"

    inject_init_id

    pp_var var

    (mpfr_prec ())

let pp_inject_clear pp_var fmt var =

  Format.fprintf fmt "%s(%a);"

    inject_clear_id

    pp_var var

let base_inject_op id =

  match id with

  | "+"      -> "MPFRPlus"

  | "-"      -> "MPFRMinus"

  | "*"      -> "MPFRTimes"

  | "/"      -> "MPFRDiv"

  | "uminus" -> "MPFRUminus"

  | "<="     -> "MPFRLe"

  | "<"      -> "MPFRLt"

  | ">="     -> "MPFRGe"

  | ">"      -> "MPFRGt"

  | "="      -> "MPFREq"

  | "!="     -> "MPFRNeq"

  (* Conv functions *)

  | "int_to_real" -> "MPFRint_to_real"

  | "real_to_int" -> "MPFRreal_to_int"

  | "_floor" -> "MPFRfloor"        

  | "_ceil" -> "MPFRceil"        

  | "_round" -> "MPFRround"        

  | "_Floor" -> "MPFRFloor"        

  | "_Ceiling" -> "MPFRCeiling"        

  | "_Round" -> "MPFRRound"        

  (* Math library functions *)

  | "acos" -> "MPFRacos"

  | "acosh" -> "MPFRacosh"

  | "asin" -> "MPFRasin"

  | "asinh" -> "MPFRasinh"

  | "atan" -> "MPFRatan"

  | "atan2" -> "MPFRatan2"

  | "atanh" -> "MPFRatanh"

  | "cbrt" -> "MPFRcbrt"

  | "cos" -> "MPFRcos"

  | "cosh" -> "MPFRcosh"

  | "ceil" -> "MPFRceil"

  | "erf" -> "MPFRerf"

  | "exp" -> "MPFRexp"

  | "fabs" -> "MPFRfabs"

  | "floor" -> "MPFRfloor"

  | "fmod" -> "MPFRfmod"

  | "log" -> "MPFRlog"

  | "log10" -> "MPFRlog10"

  | "pow" -> "MPFRpow"

  | "round" -> "MPFRround"

  | "sin" -> "MPFRsin"

  | "sinh" -> "MPFRsinh"

  | "sqrt" -> "MPFRsqrt"

  | "trunc" -> "MPFRtrunc"

  | "tan" -> "MPFRtan"

  | _        -> raise Not_found

let inject_op id =

  report ~level:3 (fun fmt -> Format.fprintf fmt "trying to inject mpfr into function %s@." id);

  try

    base_inject_op id

  with Not_found -> id

let homomorphic_funs =

  List.fold_right (fun id res -> try base_inject_op id :: res with Not_found -> res) Basic_library.internal_funs []

let is_homomorphic_fun id =

  List.mem id homomorphic_funs

let inject_call expr =

  match expr.expr_desc with

  | Expr_appl (id, args, None) when not (Basic_library.is_expr_internal_fun expr) ->

    { expr with expr_desc = Expr_appl (inject_op id, args, None) }

  | _ -> expr

let expr_of_const_array expr =

  match expr.expr_desc with

  | Expr_const (Const_array cl) ->

    let typ = Types.array_element_type expr.expr_type in

    let expr_of_const c =

      { expr_desc = Expr_const c;

	expr_type = typ;

	expr_clock = expr.expr_clock;

	expr_loc = expr.expr_loc;

	expr_delay = Delay.new_var ();

	expr_annot = None;

	expr_tag = new_tag ();

      }

    in { expr with expr_desc = Expr_array (List.map expr_of_const cl) }

  | _                           -> assert false

(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)

let rec inject_list alias node inject_element defvars elist =

  List.fold_right

    (fun t (defvars, qlist) ->

      let defvars, norm_t = inject_element alias node defvars t in

      (defvars, norm_t :: qlist)

    ) elist (defvars, [])

let rec inject_expr ?(alias=true) node defvars expr =

let res =

  match expr.expr_desc with

  | Expr_const (Const_real _)  -> mk_expr_alias_opt alias node defvars expr

  | Expr_const (Const_array _) -> inject_expr ~alias:alias node defvars (expr_of_const_array expr)

  | Expr_const (Const_struct _) -> assert false

  | Expr_ident _

  | Expr_const _  -> defvars, expr

  | Expr_array elist ->

    let defvars, norm_elist = inject_list alias node (fun _ -> inject_expr ~alias:true) defvars elist in

    let norm_expr = { expr with expr_desc = Expr_array norm_elist } in

    defvars, norm_expr

  | Expr_power (e1, d) ->

    let defvars, norm_e1 = inject_expr node defvars e1 in

    let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in

    defvars, norm_expr

  | Expr_access (e1, d) ->

    let defvars, norm_e1 = inject_expr node defvars e1 in

    let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in

    defvars, norm_expr

  | Expr_tuple elist -> 

    let defvars, norm_elist =

      inject_list alias node (fun alias -> inject_expr ~alias:alias) defvars elist in

    let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in

    defvars, norm_expr

  | Expr_appl (id, args, r) ->

    let defvars, norm_args = inject_expr node defvars args in

    let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in

    mk_expr_alias_opt alias node defvars (inject_call norm_expr)

  | Expr_arrow _ -> defvars, expr

  | Expr_pre e ->

    let defvars, norm_e = inject_expr node defvars e in

    let norm_expr = { expr with expr_desc = Expr_pre norm_e } in

    defvars, norm_expr

  | Expr_fby (e1, e2) ->

    let defvars, norm_e1 = inject_expr node defvars e1 in

    let defvars, norm_e2 = inject_expr node defvars e2 in

    let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in

    defvars, norm_expr

  | Expr_when (e, c, l) ->

    let defvars, norm_e = inject_expr node defvars e in

    let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in

    defvars, norm_expr

  | Expr_ite (c, t, e) ->

    let defvars, norm_c = inject_expr node defvars c in

    let defvars, norm_t = inject_expr node defvars t in

    let defvars, norm_e = inject_expr node defvars e in

    let norm_expr = { expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) } in

    defvars, norm_expr

  | Expr_merge (c, hl) ->

    let defvars, norm_hl = inject_branches node defvars hl in

    let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in

    defvars, norm_expr

in

(*Format.eprintf "inject_expr %B %a = %a@." alias Printers.pp_expr expr Printers.pp_expr (snd res);*)

res

and inject_branches node defvars hl =

 List.fold_right

   (fun (t, h) (defvars, norm_q) ->

     let (defvars, norm_h) = inject_expr node defvars h in

     defvars, (t, norm_h) :: norm_q

   )

   hl (defvars, [])

let rec inject_eq node defvars eq =

  let (defs', vars'), norm_rhs = inject_expr ~alias:false node defvars eq.eq_rhs in

  let norm_eq = { eq with eq_rhs = norm_rhs } in

  norm_eq::defs', vars'

(* let inject_eexpr ee =

 *   { ee with eexpr_qfexpr = inject_expr ee.eexpr_qfexpr }

 *   

 * let inject_spec s =

 *   { s with

 *     assume = List.map inject_eexpr s.assume;

 *     guarantees = List.map inject_eexpr s.guarantees;

 *     modes = List.map (fun m ->

 *                 { m with

 *                   require = List.map inject_eexpr m.require;

 *                   ensure = List.map inject_eexpr m.ensure

 *                 }

 *               ) s.modes

 *   } *)

(** normalize_node node returns a normalized node, 

    ie. 

    - updated locals

    - new equations

    - 

*)

let inject_node node = 

  cpt_fresh := 0;

  let inputs_outputs = node.node_inputs@node.node_outputs in

  let norm_ctx = (node.node_id, get_node_vars node) in

  let is_local v =

    List.for_all ((!=) v) inputs_outputs in

  let orig_vars = inputs_outputs@node.node_locals in

  let defs, vars =

    let eqs, auts = get_node_eqs node in

    if auts != [] then assert false; (* Automata should be expanded by now. *)

    List.fold_left (inject_eq norm_ctx) ([], orig_vars) eqs in

  (* Normalize the asserts *)

  let vars, assert_defs, asserts = 

    List.fold_left (

    fun (vars, def_accu, assert_accu) assert_ ->

      let assert_expr = assert_.assert_expr in

      let (defs, vars'), expr = 

	inject_expr 

	  ~alias:false 

	  norm_ctx 

	  ([], vars) (* defvar only contains vars *)

	  assert_expr

      in

      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu

    ) (vars, [], []) node.node_asserts in

  let new_locals = List.filter is_local vars in

  (* Compute traceability info: 

     - gather newly bound variables

     - compute the associated expression without aliases     

  *)

  (* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals)) new_locals in *)

  (* See comment below

   *  let spec = match node.node_spec with

   *   | None -> None

   *   | Some spec -> Some (inject_spec spec)

   * in *)

  let node =

  { node with 

    node_locals = new_locals; 

    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);

    (* Incomplete work: TODO. Do we have to inject MPFR code here?

       Does it make sense for annotations? For me, only if we produce

       C code for annotations. Otherwise the various verification

       backend should have their own understanding, but would not

       necessarily require this additional normalization. *)

    (* 

       node_spec = spec;

       node_annot = List.map (fun ann -> {ann with

           annots = List.map (fun (ids, ee) -> ids, inject_eexpr ee) ann.annots}

         ) node.node_annot *)

  }

  in ((*Printers.pp_node Format.err_formatter node;*) node)

let inject_decl decl =

  match decl.top_decl_desc with

  | Node nd ->

    {decl with top_decl_desc = Node (inject_node nd)}

  | Include _ | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl

let inject_prog decls = 

  List.map inject_decl decls

(* Local Variables: *)

(* compile-command:"make -C .." *)

(* End: *)

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)

val to_q: t -> Q.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)