/ - Diff - LustreC

         self
     let print_stateless_prototype fmt (name, inputs, outputs) =
     match outputs with
     (* DOESN'T WORK FOR ARRAYS
       | [o] -> fprintf fmt "%a (@[<v>%a@])"
         (pp_c_type name) o.var_type
         (Utils.fprintf_list ~sep:",@ " pp_c_var) inputs
     *)
       | _ -> fprintf fmt "void %s (@[<v>@[%a%t@]@,@[%a@]@,@])"
       fprintf fmt "void %s (@[<v>@[%a%t@]@,@[%a@]@,@])"
         name
         (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs
         (Utils.pp_final_char_if_non_empty ",@ " inputs)
-...
     (*                         Header Printing functions                                        *)
     (********************************************************************************************)
     (* Removed because of "open" constructs. No more extern functions *)
     (*
     let print_prototype fmt decl =
       match decl.top_decl_desc with
         | ImportedFun m -> (
             fprintf fmt "extern %a;@,"
     	  print_stateless_prototype
     	  (m.fun_id, m.fun_inputs, m.fun_outputs)
+        )
         | ImportedNode m -> (
           if m.nodei_stateless then (* It's a function not a node *)
             fprintf fmt "extern %a;@,"
     	  print_stateless_prototype
     	  (m.nodei_id, m.nodei_inputs, m.nodei_outputs)
           else (
     	let static = List.filter (fun v -> v.var_dec_const) m.nodei_inputs in
             fprintf fmt "extern %a;@,"
     	  print_alloc_prototype (m.nodei_id, static);
     	fprintf fmt "extern %a;@,"
     	  (print_reset_prototype "self") (m.nodei_id, static);
     	fprintf fmt "extern %a;@,"
     	  (print_step_prototype "self") (m.nodei_id, m.nodei_inputs, m.nodei_outputs);
+          )
+        )
         | _ -> () (* We don't do anything here *)
           *)
     let print_import_standard fmt =
       fprintf fmt "#include \"%s/include/lustrec/arrow.h\"@.@." Version.prefix
     let print_prototype fmt decl =
     let print_import_prototype fmt decl =
       match decl.top_decl_desc with
       | Open m -> fprintf fmt "#include \"%s.h\"@," m
       | _ -> () (* We don't do anything here *)
-...
         ()
     let print_machine_struct fmt m =
       if m.mname.node_id != arrow_id
       then (
         (* We don't print arrow function *)
         (* Define struct *)
         fprintf fmt "@[%a {@[%a%a%t@]};@]@."
           pp_machine_memtype_name m.mname.node_id
           pp_registers_struct m
           (Utils.fprintf_list ~sep:"; " pp_c_decl_instance_var) m.minstances
           (Utils.pp_final_char_if_non_empty "; " m.minstances)
+      )
       if fst (get_stateless_status m) then
         begin
         end
       else
         begin
           (* Define struct *)
           fprintf fmt "@[%a {@[%a%a%t@]};@]@."
     	pp_machine_memtype_name m.mname.node_id
     	pp_registers_struct m
     	(Utils.fprintf_list ~sep:"; " pp_c_decl_instance_var) m.minstances
     	(Utils.pp_final_char_if_non_empty "; " m.minstances)
         end
     (*
     let pp_static_array_instance fmt m (v, m) =
      fprintf fmt "%s" (mk_addr_var m v)
     *)
     let print_static_declare_instance attr fmt (i, (m, static)) =
       fprintf fmt "%a(%s, %a%t%s)"
         pp_machine_static_declare_name (node_name m)
-...
         pp_machine_static_link_name m.mname.node_id
     let print_machine_decl fmt m =
       if m.mname.node_id <> arrow_id
       then (
         (* We don't print arrow function *)
         (* Static allocation *)
         if !Options.static_mem
         then (
           fprintf fmt "%a@.%a@.%a@."
     	print_static_declare_macro m
     	print_static_link_macro m
     	print_static_alloc_macro m
+        )
         else (
         (* Dynamic allocation *)
       if fst (get_stateless_status m) then
         begin
           (* Print specification if any *)
           (match m.mspec with
           | None -> ()
           | Some spec ->
     	pp_acsl_spec m.mstep.step_outputs fmt spec
           );
           fprintf fmt "extern %a;@.@."
     	print_alloc_prototype (m.mname.node_id, m.mstatic)
         );
         let self = mk_self m in
         fprintf fmt "extern %a;@.@."
           (print_reset_prototype self) (m.mname.node_id, m.mstatic);
         (* Print specification if any *)
         (match m.mspec with
     	print_stateless_prototype
     	(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
         end
       else
         begin
           (* Static allocation *)
           if !Options.static_mem
           then (
     	fprintf fmt "%a@.%a@.%a@."
     	  print_static_declare_macro m
     	  print_static_link_macro m
     	  print_static_alloc_macro m
+          )
           else (
             (* Dynamic allocation *)
     	fprintf fmt "extern %a;@.@."
     	  print_alloc_prototype (m.mname.node_id, m.mstatic)
           );
           let self = mk_self m in
           fprintf fmt "extern %a;@.@."
     	(print_reset_prototype self) (m.mname.node_id, m.mstatic);
           (* Print specification if any *)
           (match m.mspec with
           | None -> ()
           | Some spec ->
     	pp_acsl_spec m.mstep.step_outputs fmt spec
         );
         fprintf fmt "extern %a;@.@."
           (print_step_prototype self)
           (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
+      )
           );
           fprintf fmt "extern %a;@.@."
     	(print_step_prototype self)
     	(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
         end
     (********************************************************************************************)
-...
         (Utils.fprintf_list ~sep:"" print_alloc_array) array_mem
         (Utils.fprintf_list ~sep:"" print_alloc_instance) m.minstances
     let print_stateless_code fmt m =
       let self = "__ERROR__" in
       if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc })
       then
         (* C99 code *)
         fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@."
           print_stateless_prototype (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
           (* locals *)
           (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) m.mstep.step_locals
           (Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals)
           (* check assertions *)
           (pp_c_checks self) m
           (* instrs *)
           (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) m.mstep.step_instrs
           (Utils.pp_newline_if_non_empty m.mstep.step_instrs)
           (fun fmt -> fprintf fmt "return;")
       else
         (* C90 code *)
         let (gen_locals, base_locals) = List.partition (fun v -> Types.is_generic_type v.var_type) m.mstep.step_locals in
         let gen_calls = List.map (fun e -> let (id, _, _) = call_of_expr e in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
         fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@."
           print_stateless_prototype (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs)
           (* locals *)
           (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) base_locals
           (Utils.pp_final_char_if_non_empty ";" base_locals)
           (* check assertions *)
           (pp_c_checks self) m
           (* instrs *)
           (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) m.mstep.step_instrs
           (Utils.pp_newline_if_non_empty m.mstep.step_instrs)
           (fun fmt -> fprintf fmt "return;")
     let print_step_code fmt m self =
       if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc })
       then
-...
           (fun fmt -> fprintf fmt "return;")
     let print_machine fmt m =
       if m.mname.node_id <> arrow_id
       then (
       (* We don't print arrow function *)
       (* Alloc function, only if non static mode *)
         if (not !Options.static_mem) then
+          (
     	fprintf fmt "@[<v 2>%a {@,%a@]@,}@.@."
     	  print_alloc_prototype (m.mname.node_id, m.mstatic)
     	  print_alloc_code m;
           );
         let self = mk_self m in
         (* Reset function *)
         fprintf fmt "@[<v 2>%a {@,%a%treturn;@]@,}@.@."
           (print_reset_prototype self) (m.mname.node_id, m.mstatic)
           (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) m.minit
           (Utils.pp_newline_if_non_empty m.minit);
         (* Step function *)
         print_step_code fmt m self
+      )
       if fst (get_stateless_status m) then
         begin
           (* Step function *)
           print_stateless_code fmt m
         end
       else
         begin
           (* Alloc function, only if non static mode *)
           if (not !Options.static_mem) then
+    	(
     	  fprintf fmt "@[<v 2>%a {@,%a@]@,}@.@."
     	    print_alloc_prototype (m.mname.node_id, m.mstatic)
     	    print_alloc_code m;
     	);
           let self = mk_self m in
           (* Reset function *)
           fprintf fmt "@[<v 2>%a {@,%a%treturn;@]@,}@.@."
     	(print_reset_prototype self) (m.mname.node_id, m.mstatic)
     	(Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) m.minit
     	(Utils.pp_newline_if_non_empty m.minit);
           (* Step function *)
           print_step_code fmt m self
         end
     (********************************************************************************************)
     (*                         Main related functions                                           *)
-...
       (* Print the prototype of imported nodes *)
       fprintf source_fmt "/* Imported nodes declarations */@.";
       fprintf source_fmt "@[<v>";
       List.iter (print_prototype source_fmt) prog;
       List.iter (print_import_prototype source_fmt) prog;
       fprintf source_fmt "@]@.";
       (* Print consts *)
       fprintf source_fmt "/* Global constants (definitions) */@.";

          mutable node_checks: Dimension.dim_expr list;
          node_asserts: assert_t list;
          node_eqs: eq list;
          node_dec_stateless: bool;
          mutable node_dec_stateless: bool;
          mutable node_stateless: bool option;
          node_spec: LustreSpec.node_annot option;
          node_annot: LustreSpec.expr_annot option;
-...
       | No_main_specified
       | Unbound_symbol of ident
       | Already_bound_symbol of ident
       | Stateful of ident
     exception Error of Location.t * error
-...
       | ImportedNode nd -> true
       | _ -> assert false
     let rec is_stateless_expr expr =
       match expr.expr_desc with
       | Expr_const _
       | Expr_ident _ -> true
       | Expr_tuple el
       | Expr_array el -> List.for_all is_stateless_expr el
       | Expr_access (e1, _)
       | Expr_power (e1, _) -> is_stateless_expr e1
       | Expr_ite (c, t, e) -> is_stateless_expr c && is_stateless_expr t && is_stateless_expr e
       | Expr_arrow (e1, e2)
       | Expr_fby (e1, e2) -> is_stateless_expr e1 && is_stateless_expr e2
       | Expr_pre e' -> is_stateless_expr e'
       | Expr_when (e', i, l)-> is_stateless_expr e'
       | Expr_merge (i, hl) -> List.for_all (fun (t, h) -> is_stateless_expr h) hl
       | Expr_appl (i, e', i') ->
         is_stateless_expr e' &&
           (Basic_library.is_internal_fun i || check_stateless_node (node_from_name i))
       | Expr_uclock _
       | Expr_dclock _
       | Expr_phclock _ -> assert false
     and compute_stateless_node nd =
      List.for_all (fun eq -> is_stateless_expr eq.eq_rhs) nd.node_eqs
     and check_stateless_node td =
       match td.top_decl_desc with
       | Node nd         -> (
         match nd.node_stateless with
         | None     ->
           begin
     	let stateless = compute_stateless_node nd in
     	nd.node_stateless <- Some (false && stateless);
     	if nd.node_dec_stateless && (not stateless)
     	then raise (Error (td.top_decl_loc, Stateful nd.node_id))
     	else stateless
           end
         | Some stl -> stl)
       | ImportedNode nd -> nd.nodei_stateless
       | _ -> true
     (* alias and type definition table *)
     let type_table =
-...
         fprintf fmt
           "%s is already defined.@."
           sym
       | Stateful nd ->
         fprintf fmt
           "node %s is declared stateless, but it is stateful.@."
           nd
     (* filling node table with internal functions *)
     let vdecls_of_typ_ck cpt ty =

          mutable node_checks: Dimension.dim_expr list;
          node_asserts: assert_t list;
          node_eqs: eq list;
          node_dec_stateless: bool;
          mutable node_dec_stateless: bool;
          mutable node_stateless: bool option;
          node_spec: LustreSpec.node_annot option;
          node_annot: LustreSpec.expr_annot option;}
-...
       | No_main_specified
       | Unbound_symbol of ident
       | Already_bound_symbol of ident
       | Stateful of ident
     exception Error of Location.t * error
-...
     val node_inputs: top_decl -> var_decl list
     val node_from_name: ident -> top_decl
     val is_generic_node: top_decl -> bool
     val check_stateless_node: top_decl -> bool
     val is_imported_node: top_decl -> bool
     val consts_table: (ident, const_desc) Hashtbl.t
-...
     val sort_handlers : (label * 'a) list -> (label * 'a) list
     val is_stateless_expr: expr -> bool
     val is_eq_expr: expr -> expr -> bool
     val pp_error :  Format.formatter -> error -> unit

         (Utils.fprintf_list ~sep:"@ " pp_instr) m.minit
         pp_step m.mstep
     (* Returns the declared stateless status and the computed one. *)
     let get_stateless_status m =
      (m.mname.node_dec_stateless, Utils.desome m.mname.node_stateless)
     let is_output m id =
       List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
-...
       fun caller callee tag ->
         begin
           let o =
     	if Corelang.check_stateless_node callee then
     	if Stateless.check_node callee then
     	  node_name callee
     	else
     	  Printf.sprintf "ni_%d" (incr cpt; !cpt) in
-...
           NodeDep.filter_static_inputs (node_inputs node_f) el in
         let o = new_instance node node_f eq.eq_rhs.expr_tag in
         (m,
          (if check_stateless_node node_f then si else MReset o :: si),
          (if Stateless.check_node node_f then si else MReset o :: si),
          (if Basic_library.is_internal_fun f then j else Utils.IMap.add o call_f j),
          d,
          reset_instance node args o r eq.eq_rhs.expr_clock @
-...
         mname = nd;
         mmemory = ISet.elements m;
         mcalls = mmap;
         minstances = List.filter (fun (_, (n,_)) -> not (check_stateless_node n)) mmap;
         minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap;
         minit = init;
         mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
         mstep = {
-...
     let translate_prog decls =
       let nodes = get_nodes decls in
        (* What to do with Imported/Sensor/Actuators ? *)
        arrow_machine ::  List.map translate_decl nodes
        (*arrow_machine ::*)  List.map translate_decl nodes
     let get_machine_opt name machines =
       List.fold_left

     let check_stateless_decls decls =
       report ~level:1 (fun fmt -> fprintf fmt ".. checking stateless/stateful status@,@?");
       try
         List.iter (fun td -> ignore (Corelang.check_stateless_node td)) decls
       with (Corelang.Error (loc, err)) as exc ->
         Stateless.check_prog decls
       with (Stateless.Error (loc, err)) as exc ->
         Format.eprintf "Stateless status error at loc %a: %a@]@."
           Location.pp_loc loc
           Corelang.pp_error err;
           Stateless.pp_error err;
         raise exc
     let type_decls env decls =
-...
           Typing.uneval_prog_generics prog;
           (* checking clocks compatibility with computed clocks*)
           Clock_calculus.check_env_compat header declared_clocks_env computed_clocks_env;
           Clock_calculus.uneval_prog_generics prog
           Clock_calculus.uneval_prog_generics prog;
           (* checking stateless status compatibility *)
           Stateless.check_compat header
         with Sys_error _ -> (
           (* Printing lusi file is necessary *)
           report ~level:1
-...
           Format.eprintf "Clock mismatch between computed clock and declared clock in lustre interface file: %a@]@."
     	Clocks.pp_error err;
           raise exc
         | Stateless.Error (loc, err) as exc ->
           Format.eprintf "Stateless status mismatch between defined status and declared status in lustre interface file: %a@]@."
     	Stateless.pp_error err;
           raise exc
       in
       (* Computes and stores generic calls for each node,

       try
         match (Hashtbl.find hashtbl name).top_decl_desc, value.top_decl_desc with
         | Node _        , ImportedNode _ when own
                             ->
            Hashtbl.add hashtbl name value
                             -> ()
         | ImportedNode _, _ ->
            Hashtbl.add hashtbl name value
         | Node _        , _ ->

       match decl.top_decl_desc with
       | Node nd ->
         fprintf fmt
           "@[<v>node %s (%a) returns (%a);@ @]@ "
           "@[<v>%s %s (%a) returns (%a);@ @]@ "
           (if Stateless.check_node decl then "function" else "node")
           nd.node_id
           pp_node_args nd.node_inputs
           pp_node_args nd.node_outputs

     (* ----------------------------------------------------------------------------
      * SchedMCore - A MultiCore Scheduling Framework
      * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
+     *
      * This file is part of Prelude
+     *
      * Prelude is free software; you can redistribute it and/or
      * modify it under the terms of the GNU Lesser General Public License
      * as published by the Free Software Foundation ; either version 2 of
      * the License, or (at your option) any later version.
+     *
      * Prelude is distributed in the hope that it will be useful, but
      * WITHOUT ANY WARRANTY ; without even the implied warranty of
      * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
      * Lesser General Public License for more details.
+     *
      * You should have received a copy of the GNU Lesser General Public
      * License along with this program ; if not, write to the Free Software
      * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
      * USA
      *---------------------------------------------------------------------------- *)
     open Corelang
     type error =
     | Stateful_kwd of ident
     | Stateful_imp of ident
     exception Error of Location.t * error
     let rec check_expr expr =
       match expr.expr_desc with
       | Expr_const _
       | Expr_ident _ -> true
       | Expr_tuple el
       | Expr_array el -> List.for_all check_expr el
       | Expr_access (e1, _)
       | Expr_power (e1, _) -> check_expr e1
       | Expr_ite (c, t, e) -> check_expr c && check_expr t && check_expr e
       | Expr_arrow _
       | Expr_fby _
       | Expr_pre _ -> false
       | Expr_when (e', i, l)-> check_expr e'
       | Expr_merge (i, hl) -> List.for_all (fun (t, h) -> check_expr h) hl
       | Expr_appl (i, e', i') ->
         check_expr e' &&
           (Basic_library.is_internal_fun i || check_node (node_from_name i))
       | Expr_uclock _
       | Expr_dclock _
       | Expr_phclock _ -> assert false
     and compute_node nd =
      List.for_all (fun eq -> check_expr eq.eq_rhs) nd.node_eqs
     and check_node td =
       match td.top_decl_desc with
       | Node nd         -> (
         match nd.node_stateless with
         | None     ->
           begin
     	let stateless = compute_node nd in
     	nd.node_stateless <- Some stateless;
     	if nd.node_dec_stateless && (not stateless)
     	then raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id))
     	else (nd.node_dec_stateless <- stateless; stateless)
           end
         | Some stl -> stl)
       | ImportedNode nd -> nd.nodei_stateless
       | _ -> true
     let check_prog decls =
       List.iter (fun td -> ignore (check_node td)) decls
     let check_compat_decl decl =
      match decl.top_decl_desc with
      | ImportedNode nd ->
        let td = Corelang.node_from_name nd.nodei_id in
        (match td.top_decl_desc with
        | Node nd' -> let stateless = check_node td in
     		 if nd.nodei_stateless && (not stateless)
     		 then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))
     		 else nd'.node_dec_stateless <- nd.nodei_stateless
        | _        -> assert false)
      | Node _          -> assert false
      | _               -> ()
     let check_compat header =
       List.iter check_compat_decl header
     let pp_error fmt err =
       match err with
       | Stateful_kwd nd ->
         Format.fprintf fmt
           "node %s should be stateless but is actually stateful.@."
           nd
       | Stateful_imp nd ->
         Format.fprintf fmt
           "node %s is declared stateless but is actually stateful.@."
           nd
     (* Local Variables: *)
     (* compile-command:"make -C .." *)
     (* End: *)

Project

General

Profile

CristalCaveGem » LustreC

Revision 5538b7ac

Added by Xavier Thirioux about 11 years ago