CristalCaveGem » LustreC

    pp_machine_memtype_name m.mname.node_id

    pp_registers_struct m

    (Utils.fprintf_list ~sep:"; " pp_c_decl_instance_var) m.minstances

(*

let pp_static_array_instance fmt m (v, m) =

 fprintf fmt "%s" (mk_addr_var m v)

  (* Print the svn version number and the supported C standard (C90 or C99) *)

  print_version header_fmt;

  fprintf header_fmt "#ifndef _%s@.#define _%s@." baseNAME baseNAME;

  fprintf header_fmt "/* Struct declarations */@.";

  List.iter (print_machine_struct header_fmt) machines;

  pp_print_newline header_fmt ();

  (* Print the prototypes of all machines *)

  fprintf header_fmt "/* Nodes declarations */@.";

  List.iter (print_machine_decl header_fmt) machines;

    raise (Error (loc, Clock_extrusion (ck_node, ck)))

(* Clocks instanciation *)

  let cr = carrier_repr cr in

  match cr.carrier_desc with

  | Carry_const _

(* inst_ck_vars ensures that a polymorphic variable is instanciated with

   the same monomorphic variable if it occurs several times in the same

   type. inst_cr_vars is the same for carriers. *)

  match ck.cdesc with

  | Carrow (ck1,ck2) ->

      {ck with cdesc =

  | Ctuple cklist ->

      {ck with cdesc = Ctuple 

  | Con (ck',c,l) ->

  | Cvar _ | Pck_const (_,_) -> ck

  | Pck_up (ck',k) ->

  | Pck_down (ck',k) ->

  | Pck_phase (ck',q) ->

  | Clink ck' ->

  | Ccarrying (cr,ck') ->

        {ck with cdesc =

  | Cunivar cset ->

      try

        List.assoc ck.cid !inst_ck_vars

        with Not_found -> 

	  failwith ("Internal error, variable \""^v^"\" not found")

      in

      expr.expr_clock <- ck;

      ck

  | Expr_array elist ->

let clock_prog env decls =

  List.fold_left (fun e decl -> clock_top_decl e decl) env decls

  Env.iter declared (fun k decl_clock_k -> 

    try_unify decl_clock_k computed_c Location.dummy_loc

  ) 

(* Local Variables: *)

let rec normalize dim =

 dim

let copy copy_dim_vars dim =

  let rec cp dim =

  match dim.dim_desc with

  | Dvar -> ()

  | Dunivar -> assert false

  let univar = repr univar in

  match univar.dim_desc with

  | Dunivar -> univar.dim_desc <- Dident const

    begin

      try

	Typing.type_prog env decls

      with (Types.Error (loc,err)) as exc ->

	Format.eprintf "Typing error at loc %a: %a@]@."

	  Location.pp_loc loc

  Location.init lexbuf filename;

  (* Parsing *)

  report ~level:1 (fun fmt -> fprintf fmt "@[<v>.. parsing header file %s@,@?" filename);

  let new_tenv = type_decls Basic_library.type_env header in   (* Typing *)

  let new_cenv: Clocks.clock_expr Utils.IMap.t = clock_decls Basic_library.clock_env header in   (* Clock calculus *)

  header, new_tenv, new_cenv

let rec compile basename extension =

  (* Loading the input file *)

      try

	let basename = s ^ ".lusi" in 

	report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>Library %s@ " s);

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

	Env.overwrite type_env lusi_type_env,

	Env.overwrite clock_env lusi_clock_env      

    raise exc

    end;

  *)

  (* Computes and stores generic calls for each node,

     only useful for ANSI C90 compliant generic node compilation *)

  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;

  (* Normalization phase *)

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

  let normalized_prog = Normalization.normalize_prog prog in

  report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,@?" Printers.pp_prog normalized_prog);

  (* Checking array accesses *)

  if !Options.check then

    (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)

    machine_code);

  (* Printing code *)

  let _ = match !Options.output with

      "C" -> 

	begin

	  let spec_file_opt = if !Options.c_spec then 

	      (

		let spec_file = basename ^ "_spec.c" in

	    | Some f -> Some (formatter_of_out_channel (open_out f))

	  in

	  report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,@?");

	end

    (*let source_file = basename ^ ".java" in

      report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);

      let source_out = open_out source_file in

      let source_fmt = formatter_of_out_channel source_out in

      report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");

      Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)

    | _ -> assert false

  in

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

let check = ref false

let c_spec = ref false

let output = ref "C"

let verbose_level = ref 1

let global_inline = ref false

let witnesses = ref false

let options =

  [ "-d", Arg.Set_string dest_dir,

    "-node", Arg.Set_string main_node, "specifies the main node";

    "-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes";

    "-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node (default: static)";

    "-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds (default: no check)";

    "-c-spec", Arg.Set c_spec, 

    "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";

%%

prog:

header:

top_decl_list:

  top_decl {[$1]}

    in

    Hashtbl.add node_table $3 nd; nd}

nodespec_list:

NODESPEC { $1 }

| NODESPEC nodespec_list { LustreSpec.merge_node_annot $1 $2 }

    | Const_tag  t -> pp_print_string fmt t

    | Const_array ca -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca

and pp_expr fmt expr =

  match expr.expr_desc with

let pp_node_eqs = fprintf_list ~sep:"@ " pp_node_eq 

let pp_var_type_dec fmt ty =

  let rec pp_var_type_dec_desc fmt tdesc =

  match locals with [] -> () | _ ->

    fprintf fmt "@[<v 4>var %a@]@ " 

      (fprintf_list ~sep:"@ " 

      locals

  ) nd.node_locals

  (fun fmt checks ->

  | Tunivar ->

    fprintf fmt "'%s" (name_of_type ty.tid)

let pp_error fmt = function

  | Unbound_value id ->

    fprintf fmt "Unknown value %s@." id

        t2.tdesc <- Tlink t1

    | Tarrow (t1,t2), Tarrow (t1',t2') ->

      begin

      end

    | Ttuple tlist1, Ttuple tlist2 ->

        if (List.length tlist1) <> (List.length tlist2) then

    | Tarray (e1, t1'), Tarray (e2, t2') ->

      begin

	semi_unify t1' t2';

	Dimension.semi_unify e1 e2;

      end

    | _,_ -> raise (Unify (t1, t2))

  | Dimension.Unify _ ->

    raise (Error (loc, Type_clash (ty1,ty2)))

let rec type_const loc c = 

  match c with

  | Const_int _ -> Type_predef.type_int

		 expr_annot = None})

          dummy_id_expr cl

      in

      ignore (type_expr env false false when_expr)

let rec check_type_declaration loc cty =

let uneval_prog_generics prog =

 List.iter uneval_top_generics prog

  Env.iter declared (fun k decl_type_k -> 

  ) 

(* Local Variables: *)

const MatrixAddition_Constant_Value = [ [ 2, 3, 4 ], [ 5, 6, 7 ] ] ;

const MatrixAddition_Constant1_Value = [ [ 8, 9, 10 ], [ 11, 12, 13 ] ] ;

const MatrixAddition_Constant2_Value = [ [ 2, 3, 4 ] ] ;

#LUSTREC="../../_build/src/lustrec"

LUSTREC=lustrec

mkdir -p build

while IFS=, read -r file main opts

do

  echo fichier:$file

#   echo main:$main

    rm -f witness*

    if [ "$main" != "" ]; then

        if [ $? -ne 0 ]; then

          rlustrec1="INVALID";

        else

          rlustrec1="VALID"

	fi

        if [ $? -ne 0 ]; then

          rgcc1="INVALID";

        else

          rgcc1="VALID"

	fi	

	# Removing Generated lusi file

	# Checking inlining

	if [ $? -ne 0 ]; then

          rlustrec2="INVALID";

        else

          rlustrec2="VALID"

	fi

        if [ $? -ne 0 ]; then

          rgcc2="INVALID";

        else

          rgcc2="VALID"

	fi	

	# Cheching witness

	lustreh -horn -node check witness.lus 2>/dev/null

    	z3="`z3 -t:10 witness.smt2 | xargs`"

    	if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then

	  rinlining="VALID";

	 exit 1

        fi  

	# Checking horn backend

	# TODO: This part of the script has to be optimized

	if [ $? -ne 0 ]; then

         rhorn="INVALID";

        else

        fi

	echo "lustrec ($rlustrec1),gcc($rgcc1),lustrec inline ($rlustrec2), gcc inline ($rgcc2), inlining valid ($rinlining),horn ($rhorn),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN"

    else

        if [ $? -ne 0 ]; then

          rlustrec1="INVALID";

        else

          rlustrec1="VALID"

        fi

        if [ $? -ne 0 ]; then

          rgcc1="INVALID";

        else

          rgcc1="VALID"

        fi

	echo "lustrec ($rlustrec1), gcc($rgcc1), horn($rhorn), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN"

    fi