CristalCaveGem » LustreC

BIN_TARGETS = lustrec lustret lustrev @lustresf_target@

lustrev:

	@echo Compiling binary lustrev

	@make -C src lustrev

AC_MSG_CHECKING(ocaml libraries required (ocamlgraph cmdliner fmt logs num)) 

# Seal

AC_MSG_CHECKING(seal library (optional))

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

])

# z3

AC_MSG_CHECKING(z3 library (optional))

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

    [z3=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],

)

AS_IF([test "x$z3" = "xyes"], [

   AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);")

   AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package(z3)")

])

# 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"], [

   AC_SUBST(LUSTREV_TINY, "(module Tiny_verifier.Verifier : VerifierType.S);")

   AC_SUBST(LUSTREV_TINY_TAG, "<**/*>: package(tiny)")

])

   AC_SUBST(SALSA, "(module Salsa_plugin.Plugin : PluginType.S);")

		 src/verifierList.ml

AC_MSG_NOTICE(********   Verifiers    ********)

  if (test "x$seal" = "xyes"); then

      AC_MSG_NOTICE([Seal   enabled])

  else

      AC_MSG_NOTICE([Seal   disabled. Require Seal library])

  fi

  if (test "x$z3" = xyes); then

      AC_MSG_NOTICE([Zustre enabled])

  else

      AC_MSG_NOTICE([Zustre disabled. Require Z3 ocaml library])

  fi

  if (test "x$tiny" = xyes); then

      AC_MSG_NOTICE([Tiny   enabled])

  else

      AC_MSG_NOTICE([Tiny   disabled. Require Tiny library])

  fi

all: lustrec lustret lustrev

lustrev:

	@echo Compiling binary lustrev

	@$(OCAMLBUILD) main_lustre_verifier.native

	@mkdir -p $(LOCAL_BINDIR)

	@mv _build/main_lustre_verifier.native $(LOCAL_BINDIR)/lustrev

.PHONY: compile-lusi doc dot lustrec lustret lustrev lustrec.odocl clean install dist-clean tests

"tools": include

<**/*.native>                   : use_unix

# Available solvers

@LUSTREV_SEAL_TAG@

@LUSTREV_TINY_TAG@

@LUSTREV_Z3_TAG@

  let params = Backends.get_normalization_params () in

  let prog = Normalization.normalize_prog params prog in

let clean_al prog : program_t * bool * report =

(* Special treatment of arrows in lustre backend. We want to keep them *)

let unfold_arrow () =

  match !Options.output with

  | "lustre" -> false

  | _ -> true

(* Forcing ite normalization *)

let alias_ite () =

  match !Options.output with

  | "emf" -> true

  | _ -> false

(* Forcing basic functions normalization *)

let alias_internal_fun () =

  match !Options.output with

  | "emf" -> true

  | _ -> false

let get_normalization_params () = {

    Normalization.unfold_arrow_active = unfold_arrow ();

    force_alias_ite = alias_ite ();

    force_alias_internal_fun = alias_internal_fun ();

  }

exception StopPhase1 of program_t

	if !Options.output = "C" then Lusic.print_lusic_to_h destname lusic_ext

	  if !Options.output = "C" then Lusic.print_lusic_to_h destname lusic_ext

let stage1 params prog dirname basename =

  let prog = Normalization.normalize_prog params prog in

val pp_prog_type : Format.formatter -> program_t -> unit

val pp_prog_clock : Format.formatter -> program_t -> unit

val get_nodes : program_t -> top_decl list

val get_imported_nodes : program_t -> top_decl list

val get_consts : program_t -> top_decl list

val get_typedefs: program_t -> top_decl list

val get_dependencies : program_t -> top_decl list

(* val prog_unfold_consts: program_t -> program_t *)

val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program_t -> program_t

type program_t = top_decl list

  let params = Backends.get_normalization_params () in

      Compiler_stages.stage1 params prog dirname basename

  let params = Backends.get_normalization_params () in

  let prog, dependencies = Compiler_stages.stage1 params prog dirname basename in

    let params = Backends.get_normalization_params () in

    let prog_mcdc = Normalization.normalize_prog params prog_mcdc in

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

(*                                                                  *)

(*  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 Format

open Log

open Compiler_common

open Utils

open LustreSpec

let usage = "Usage: lustrev [options] \x1b[4msource file\x1b[0m"

let extensions = [".ec"; ".lus"; ".lusi"]

(* verify a .lus source file 

we have multiple "backends"

- zustre: linked to z3/spacer. Shall preserve the structure and rely on contracts. Produces both a lustre model with new properties, maybe as a lusi with lustre contract, and a JSON summarizing the results and providing tests cases or counter examples if any

- seal: linked to seal. Require global inline and main node

  focuses only on the selected node (the main)

  map the machine code into SEAL datastructure and compute invariants

  - provides the node and its information (typical point of interest for taylor expansion, range for inputs, existing invariants, computation error for the node content)

  - simplification of program through taylor expansion

  - scaling when provided with typical ranges (not required to be sound for the moment)

  - computation of lyapunov invariants

  - returns an annotated node with invariants and a JSON to explain computation

  - could also returns plots

- tiny: linked to tiny library to perform floating point analyses

  shall be provided with ranges for inputs or local variables (memories)

*)

let rec verify dirname basename extension =

  let source_name = dirname ^ "/" ^ basename ^ extension in

  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>");

  (* Parsing source *)

  let prog = parse_source source_name in

  (* Checking which solver is active *)

  let verifier = Verifiers.get_active () in

  let module Verifier = (val verifier : VerifierType.S) in

  (* Normalizing it *)

  let prog, dependencies = 

    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");

    try

      let params = Verifier.get_normalization_params () in

      Compiler_stages.stage1 params prog dirname basename

    with Compiler_stages.StopPhase1 prog -> (

        assert false

    )

  in

  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@,");

  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Normalized program:@ %a@ "Printers.pp_prog prog);

  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");

  let machine_code = 

    Compiler_stages.stage2 prog 

  in

  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");

  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ "Machine_code.pp_machines machine_code);

  if Scopes.Plugin.show_scopes () then

    begin

      let all_scopes = Scopes.compute_scopes prog !Options.main_node in

      (* Printing scopes *)

      if !Options.verbose_level >= 1 then

	Format.printf "Possible scopes are:@   ";

      Format.printf "@[<v>%a@ @]@ @?" Scopes.print_scopes all_scopes;

      exit 0

    end;

  let machine_code = Plugins.refine_machine_code prog machine_code in

  assert (dependencies = []); (* Do not handle deps yet *)

  Verifier.run basename prog machine_code;

  begin

    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");

    (* We stop the process here *)

    exit 0

  end

let anonymous filename =

  let ok_ext, ext = List.fold_left

    (fun (ok, ext) ext' ->

      if not ok && Filename.check_suffix filename ext' then

	true, ext'

      else

	ok, ext)

    (false, "") extensions in

  if ok_ext then

    let dirname = Filename.dirname filename in

    let basename = Filename.chop_suffix (Filename.basename filename) ext in

    verify dirname basename ext

  else

    raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))

let _ =

  Global.initialize ();

  Corelang.add_internal_funs ();

  try

    Printexc.record_backtrace true;

    let options = Options_management.lustrev_options @ (Verifiers.options ()) in

    Arg.parse options anonymous usage

  with

  | Parse.Error _

  | Types.Error (_,_) | Clocks.Error (_,_) -> exit 1

  | Corelang.Error (_ (* loc *), kind) (*| Task_set.Error _*) -> exit (Error.return_code kind)

  (* | Causality.Error _  -> exit (Error.return_code Error.AlgebraicLoop) *)

  | Sys_error msg -> (eprintf "Failure: %s@." msg); exit 1

  | exc -> (track_exception (); raise exc) 

(* Local Variables: *)

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

(* End: *)

type param_t =

  {

    unfold_arrow_active: bool;

    force_alias_ite: bool;

    force_alias_internal_fun: bool;

  }

let params = ref

               {

                 unfold_arrow_active = false;

                 force_alias_ite = false;

                 force_alias_internal_fun =false;

               }

      && not (!params.force_alias_internal_fun || alias_basic) ->

       mk_expr_alias_opt (alias && (!params.force_alias_internal_fun || alias_basic

  | Expr_arrow (e1,e2) when !params.unfold_arrow_active && not (is_expr_once expr) ->

  | _ when !params.force_alias_ite ->

let normalize_prog p decls =

  params := p;

  List.map normalize_decl decls

           (* Local Variables: *)

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

           (* End: *)

let lustrev_options =

   common_options @

  [ 

   "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";

    "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";

]

let verifier_opt (name, activate, options) =

  ( "-" ^ name , Arg.Unit activate, "run verifier " ^ name ) ::

    (List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options)

    (module Scopes.Plugin : PluginType.S);

module type S =

	let module M = (val m : PluginType.S) in

	let module M = (val m : PluginType.S) in

    let module M = (val m : PluginType.S) in

  List.iter (fun (m: (module PluginType.S)) -> 

    let module M = (val m : PluginType.S) in

  List.iter (fun (m: (module PluginType.S)) -> 

    let module M = (val m : PluginType.S) in

 end: PluginType.S)

    include PluginType.S

let active = ref false

module Verifier =

  (struct

    include VerifierType.Default

    let name = "seal"

    let options = []

    let activate () = active := true

    let is_active () = !active

    let run basename prog machines = ()

  end: VerifierType.S)

  type c. c call_t -> c -> t -> LustreSpec.program_t =

  val mkprincipal : t -> LustreSpec.program_t

  val mkcomponent : 'c call_t -> 'c -> t -> LustreSpec.program_t

     let params = Backends.get_normalization_params () in

     let prog, deps = Compiler_stages.stage1 params prog "" "" in

open LustreSpec

open Machine_code

open Format

open Horn_backend_common

open Horn_backend

let active = ref false

let ctx = ref (Z3.mk_context [])

let bool_sort = Z3.Boolean.mk_sort !ctx

let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx

let real_sort = Z3.Arithmetic.Real.mk_sort !ctx

let const_sorts = Hashtbl.create 13

let get_const_sort ty_name =

  Hashtbl.find const_sorts ty_name

let decl_sorts () =

  Hashtbl.iter (fun typ decl ->

    match typ with

    | Tydec_const var ->

      (match decl.top_decl_desc with

      | TypeDef tdef -> (

	match tdef.tydef_desc with

	| Tydec_enum tl ->

	  let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in

          Hashtbl.add const_sorts var new_sort

	| _ -> assert false

      )

      | _ -> assert false

      )

    | _        -> ()) Corelang.type_table

let rec type_to_sort t =

  if Types.is_bool_type t  then bool_sort else

    if Types.is_int_type t then int_sort else 

  if Types.is_real_type t then real_sort else 

  match (Types.repr t).Types.tdesc with

  | Types.Tconst ty       -> get_const_sort ty

  | Types.Tclock t        -> type_to_sort t

  | Types.Tarray(dim,ty)   -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)

  | Types.Tstatic(d, ty)-> type_to_sort ty

  | Types.Tarrow _

  | _                     -> Format.eprintf "internal error: pp_type %a@."

                               Types.print_ty t; assert false

let decl_var id =

  Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type)

let decl_machine machines m =

  if m.Machine_code.mname.node_id = Machine_code.arrow_id then

    (* We don't print arrow function *)

    ()

  else

    begin

      let _ = List.map decl_var 

      	(

	  (inout_vars machines m)@

	    (rename_current_list (full_memory_vars machines m)) @

	    (rename_mid_list (full_memory_vars machines m)) @

	    (rename_next_list (full_memory_vars machines m)) @

	    (rename_machine_list m.mname.node_id m.mstep.step_locals)

	)

      in

      ()

     (*

      if is_stateless m then

	begin

	  (* Declaring single predicate *)

	  fprintf fmt "(declare-rel %a (%a))@."

	    pp_machine_stateless_name m.mname.node_id

	    (Utils.fprintf_list ~sep:" " pp_type)

	    (List.map (fun v -> v.var_type) (inout_vars machines m));

          match m.mstep.step_asserts with

	  | [] ->

	     begin

	       (* Rule for single predicate *)

	       fprintf fmt "; Stateless step rule @.";

	       fprintf fmt "@[<v 2>(rule (=> @ ";

	       ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);

	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."

		 pp_machine_stateless_name m.mname.node_id

		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);

	     end

	  | assertsl ->

	     begin

	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in

	       fprintf fmt "; Stateless step rule with Assertions @.";

	       (*Rule for step*)

	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";

	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);

	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl

		 pp_machine_stateless_name m.mname.node_id

		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);

	     end

	end

      else

	begin

	  (* Declaring predicate *)

	  fprintf fmt "(declare-rel %a (%a))@."

	    pp_machine_reset_name m.mname.node_id

	    (Utils.fprintf_list ~sep:" " pp_type)

	    (List.map (fun v -> v.var_type) (reset_vars machines m));

	  fprintf fmt "(declare-rel %a (%a))@."

	    pp_machine_step_name m.mname.node_id

	    (Utils.fprintf_list ~sep:" " pp_type)

	    (List.map (fun v -> v.var_type) (step_vars machines m));

	  pp_print_newline fmt ();

	  (* Rule for reset *)

	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."

	    (pp_machine_reset machines) m 

	    pp_machine_reset_name m.mname.node_id

	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);

          match m.mstep.step_asserts with

	  | [] ->

	     begin

	       fprintf fmt "; Step rule @.";

	       (* Rule for step*)

	       fprintf fmt "@[<v 2>(rule (=> @ ";

	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);

	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."

		 pp_machine_step_name m.mname.node_id

		 (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);

	     end

	  | assertsl -> 

	     begin

	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in

	       (* print_string pp_val; *)

	       fprintf fmt "; Step rule with Assertions @.";

	       (*Rule for step*)

	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";

	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);

	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl

		 pp_machine_step_name m.mname.node_id

		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);

	     end

	end

      *)  end

module Verifier =

  (struct

    include VerifierType.Default

    let name = "zustre"

    let options = []

    let activate () = (

        active := true;

        Options.output := "horn";

      )

    let is_active () = !active

    let get_normalization_params () =

      (* make sure the output is "Horn" *)

      assert(!Options.output = "horn");

      Backends.get_normalization_params ()

    let run basename prog machines =

      let machines = Machine_code.arrow_machine::machines in

      let machines = preprocess machines in

      decl_sorts ();

      List.iter (decl_machine machines) (List.rev machines);

      ()

  end: VerifierType.S)

let verifiers =

  [

    @LUSTREV_SEAL@

    @LUSTREV_ZUSTRE@

    @LUSTREV_TINY@

  ]

module type S =

sig

  val name: string

  val activate: unit -> unit

  val is_active: unit -> bool

  val options: (string * Arg.spec * string) list

  val get_normalization_params: unit -> Normalization.param_t

  val run: string -> LustreSpec.program_t -> Machine_code.machine_t list -> unit 

end

module Default =

  struct

    let get_normalization_params () = {

    Normalization.unfold_arrow_active = true;

    force_alias_ite = false;

    force_alias_internal_fun = false;

  }

  end

open LustreSpec

open VerifierList

let active = ref None

let options () = 

  List.flatten (

    List.map Options_management.verifier_opt (

      List.map (fun m ->

	let module M = (val m : VerifierType.S) in

	(M.name, M.activate, M.options)

      ) verifiers

    ))

let verifier_list verifiers =

  List.fold_left (fun acc m ->

      let module M =  (val m : VerifierType.S) in

      (if acc = "" then "" else acc ^ ", ") ^ M.name

    ) "" verifiers

let get_active () =

  match !active with

  | None ->

     begin

       (* check that a single one is active and register it *)

       let found =

         List.fold_left (fun found m ->

             let module M =  (val m : VerifierType.S) in

             if M.is_active () then

               m::found

             else

               found

           ) [] verifiers

       in

       match found with

       | [] -> raise (Sys_error ("Please select one verifier in " ^ verifier_list verifiers))

       | [m] -> active := Some m; m

       | _ -> raise (Sys_error ("Too many selected verifiers: " ^ verifier_list found))

     end

  | Some m -> m

                (* Local Variables: *)

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

                (* End: *)