CristalCaveGem » LustreC

Current Status:    [![Build Status](https://travis-ci.org/coco-team/lustrec.svg?branch=master)](https://travis-ci.org/coco-team/lustrec)

# LustreC

LustreC is a modular compiler of Lustre code into C and Horn Clauses.

define([gitversion], esyscmd([sh -c "git log --oneline | wc -l | tr -d '\n'"]))

# Next release will be

AC_CONFIG_SRCDIR([src/main_lustre_compiler.ml])

# Instanciation

AC_CONFIG_FILES([Makefile

		 src/Makefile

		 src/version.ml

		 test/test-compile.sh

		 ])

int ISATTY;

/* Standard Input procedures **************/

   char b[512];

   _Bool r = 0;

   int s = 1;

      if((c == '0') || (c == 'f') || (c == 'F')) r = 0;

      if((c == '1') || (c == 't') || (c == 'T')) r = 1;

   } while((s != 1) || (r == -1));

   return r;

}

   char b[512];

   int r;

   int s = 1;

      if(scanf("%s", b)==EOF) exit(0);

      s = sscanf(b, "%d", &r);

   } while(s != 1);

   return r;

}

   char b[512];

   double r;

   int s = 1;

      if(scanf("%s", b)==EOF) exit(0);

      s = sscanf(b, "%lf", &r);

   } while(s != 1);

   return r;

}

/* Standard Output procedures **************/

  if(ISATTY) {

    printf("%s = ", n);

  } else {

  };

  printf("'%i' ", (_V)? 1 : 0);

  printf("\n");

}

  if(ISATTY) {

    printf("%s = ", n);

  } else {

  };

  printf("'%d' ", _V);

  printf("\n");

}

  if(ISATTY) {

    printf("%s = ", n);

  } else {

  };

  printf("'%f' ", _V);

  printf("\n");

}

/* Standard Input procedures **************/

/*@ assigns *n; */

/*@ assigns *n; */

/*@ assigns *n; */

/* Standard Output procedures **************/

/*@ assigns \nothing; */

/*@ assigns \nothing; */

/*@ assigns \nothing; */

#endif

backends/C/C_backend_makefile

backends/C/C_backend_spec

backends/C/C_backend_src

backends/Horn/Horn_backend

Basic_library

Causality

Clock_calculus

Delay_predef

Dimension

Env

Inliner

Lexer_lustre

LexerLustreSpec

Machine_code

Main_lustre_compiler

Modules

Normalization

Optimize_machine

Optimize_prog

Options

Parse

Parser_lustre

Printers

Scheduling

SortProg

#                  LUS_FILES <Lustre files>

#                  [USER_C_FILES <C files>]

#                  [VERBOSE <level>]

#                  LIBNAME <libraryName>)

#

# When used the Lustre_Compile macro define the variable

# Macros used to compile a lustre library

include(CMakeParseArguments)

function(Lustre_Compile)

  set(oneValueArgs NODE LIBNAME VERBOSE)

  set(multiValueArgs LUS_FILES USER_C_FILES)

  cmake_parse_arguments(LUS "${options}" "${oneValueArgs}" "${multiValueArgs}" ${ARGN})

  if (NOT LUS_LIBNAME)

    message(FATAL_ERROR "You should specify LIBNAME for each Lustre_Compile call.")

  endif()

  if(LUS_NODE)

    set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/lus_${LUS_LIBNAME}/${LUS_NODE}")

  else()

    set(LUSTRE_NODE_OPT "")

  endif()

  if (LUS_VERBOSE)

  else()

    # the default is to be quiet.

    set(LUSTRE_VERBOSE_OPT "-verbose;0")

    get_filename_component(E ${LFILE} EXT)

    if ("${E}" STREQUAL ".lus")

      set(LUSTRE_GENERATED_FILES ${LUSTRE_OUTPUT_DIR}/${L}.h ${LUSTRE_OUTPUT_DIR}/${L}.c ${LUSTRE_OUTPUT_DIR}/${L}_alloc.h)

    elseif("${E}" STREQUAL ".lusi")

      set(LUSTRE_GENERATED_FILES ${LUSTRE_OUTPUT_DIR}/${L}.h)

    endif()

    list(APPEND GLOBAL_LUSTRE_GENERATED_C_FILES ${LUSTRE_GENERATED_FILES})

    set(LUSTRE_GENERATED_FILES ${LUSTRE_GENERATED_FILES} ${LUSTRE_OUTPUT_DIR}/${L}.lusic)

    add_custom_command(

      OUTPUT ${LUSTRE_GENERATED_FILES}

      COMMAND ${LUSTRE_COMPILER} ${LUSTRE_VERBOSE_OPT} ${LUSTRE_NODE_OPT} -d ${LUSTRE_OUTPUT_DIR} ${LFILE}

  endforeach()

  include_directories(${LUSTRE_INCLUDE_DIR} ${CMAKE_CURRENT_SOURCE_DIR} ${LUSTRE_OUTPUT_DIR})

  add_library(${LUS_LIBNAME} SHARED

              ${GLOBAL_LUSTRE_GENERATED_C_FILES} ${LUS_USER_C_FILES}

              )

  set_target_properties(${LUS_LIBNAME} PROPERTIES COMPILE_FLAGS "-std=c99")

  set(LUSTRE_GENERATED_C_FILES_${LUS_LIBNAME} "${GLOBAL_LUSTRE_GENERATED_C_FILES}" PARENT_SCOPE)

  message(STATUS "Lustre: Added rule for building lustre library: ${LUS_LIBNAME}")

"backends/Horn": include

<**/.svn>: -traverse

<**/.svn>: not_hygienic

"main_lustre_compiler.native": use_str

"main_lustre_compiler.native": use_unix

<*.ml{,i}>: use_str

<*.ml{,i}>: use_unix

let gen_files funs basename prog machines dependencies =

  let destname = !Options.dest_dir ^ "/" ^ basename in

  (* Generating H file *)

  let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)

  let header_fmt = formatter_of_out_channel header_out in

  print_header header_fmt basename prog machines dependencies;

  close_out header_out;

  (* Generating Lib C file *)

  let source_lib_file = destname ^ ".c" in (* Could be changed *)

  let source_lib_out = open_out source_lib_file in

  print_lib_c source_lib_fmt basename prog machines dependencies;

  close_out source_lib_out;

  | main_node -> (

    match Machine_code.get_machine_opt main_node machines with

    | None -> begin

      raise (Corelang.Error (Location.dummy_loc, LustreSpec.Main_not_found))

    end

    | Some m -> begin

      let source_main_out = open_out source_main_file in

      let source_main_fmt = formatter_of_out_channel source_main_out in

      (* Generating Main C file *)

      print_main_c source_main_fmt m basename prog machines dependencies;

    end

let translate_to_c basename prog machines dependencies =

  match !Options.spec with

    let module Source = C_backend_src.Main (SourceMod) in

    let module SourceMain = C_backend_main.Main (SourceMainMod) in

    let module Makefile = C_backend_makefile.Main (MakefileMod) in

    in

  end

  | "acsl" -> begin

    let module Source = C_backend_src.Main (SourceMod) in

    let module SourceMain = C_backend_main.Main (SourceMainMod) in

    let module Makefile = C_backend_makefile.Main (MakefileMod) in

      Source.print_lib_c,

      SourceMain.print_main_c,

    in

  end

  | "c" -> begin

      begin

	fprintf fmt "#include <mpfr.h>@."

      end;

  end

let rec print_static_val pp_var fmt v =

open Machine_code

open Format

open C_backend_common

module type MODIFIERS_MAINSRC =

sig

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

let print_get_inputs fmt m =

  match (Types.unclock_type v.var_type).Types.tdesc with

    | _ ->

      begin

	Global.main_node := !Options.main_node;

	raise (Error (v'.var_loc, Main_wrong_kind))

      end

  in

let print_put_outputs fmt m = 

    match (Types.unclock_type o.var_type).Types.tdesc with

    | _ -> assert false

  in

let print_main_memory_allocation mname main_mem fmt m =

  if not (fst (get_stateless_status m)) then

  begin  

    fprintf fmt "@ /* Infinite loop */@ ";

    fprintf fmt "@[<v 2>while(1){@ ";

    fprintf fmt  "fflush(stdout);@ ";

    fprintf fmt "%a@ %t%a"

      print_get_inputs m

      (fun fmt -> pp_main_call mname main_mem fmt m input_values m.mstep.step_outputs)

    then "&main_mem"

    else "main_mem" in

  fprintf fmt "@[<v 2>int main (int argc, char *argv[]) {@ ";

  print_main_memory_allocation mname main_mem fmt m;

  if !Options.mpfr then

    begin

  fprintf fmt "@]@ }@."       

let print_main_header fmt =

let print_main_c main_fmt main_machine basename prog machines _ (*dependencies*) =

    )

end

let print_type_definitions fmt =

  let cpt_type = ref 0 in

  Hashtbl.iter (fun typ decl ->

    | _        -> ()) type_table

  (* We print typedef *)

  print_type_definitions fmt;

  main_print machines fmt

(* Local Variables: *)

  | Types.Treal           -> fprintf fmt "Real"

  | Types.Tconst ty       -> pp_print_string fmt ty

  | Types.Tclock t        -> pp_type fmt t

  | Types.Tarrow _

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

    Types.print_ty t; assert false

let local_memory_vars machines machine =

  rename_machine_list machine.mname.node_id machine.mmemory

let instances_memory_vars ?(without_arrow=false) machines machine =

  let rec aux fst prefix m =

    (

      List.fold_left (fun accu (id, (n, _)) ->

	let name = node_name n in

	if without_arrow && name = "_arrow" then

	else

	  let machine_n = get_machine machines name in

			 (if fst then id else concat m.mname.node_id id))

	      machine_n ) @ accu

      ) [] (m.minstances)

let step_vars machines m =

  (inout_vars machines m)

  @ (rename_next_list (full_memory_vars machines m))

let step_vars_m_x machines m =

  (inout_vars machines m)

  @ (rename_next_list (full_memory_vars machines m))

let reset_vars machines m =

  @ (rename_mid_list (full_memory_vars machines m))

open Machine_code

open Horn_backend_common

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

(*                    Instruction Printing functions                                        *)

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

let pp_horn_var m fmt id =

  then

    assert false (* no arrays in Horn output *)

    fprintf fmt "%s" id.var_id

(* Used to print boolean constants *)

    | Const_tag t    -> pp_horn_tag fmt t

    | _              -> assert false

(* Prints a value expression [v], with internal function calls only.

   [pp_var] is a printer for variables (typically [pp_c_var_read]),

   but an offset suffix may be added for array variables

*)

let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =

  match v.value_desc with

(* Prints a [value] indexed by the suffix list [loop_vars] *)

let rec pp_value_suffix self pp_value fmt value =

*)

let pp_assign m pp_var fmt var_name value =

  let self = m.mname.node_id in

    (pp_horn_val ~is_lhs:true self pp_var) var_name

    (pp_value_suffix self pp_var) value

(* In case of no reset call, we define mid_mem = current_mem *)

let pp_no_reset machines m fmt i =

  let (n,_) = List.assoc i m.minstances in

  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in

    rename_machine_list

      (concat m.mname.node_id i)

      (rename_mid_list (full_memory_vars machines target_machine))

    fprintf fmt "(= %a %a)"

      (pp_horn_var m) mhd

      (pp_horn_var m) chd

  | _ -> (

    fprintf fmt "@[<v 0>(and @[<v 0>";

      fprintf fmt "(= %a %a)@ "

      (pp_horn_var m) mhd

      (pp_horn_var m) chd

let pp_instance_reset machines m fmt i =

  let (n,_) = List.assoc i m.minstances in

  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in

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

    pp_machine_reset_name (node_name n)

    (

      (rename_machine_list

	 (concat m.mname.node_id i)

	 (rename_current_list (full_memory_vars machines target_machine))

      @

	(rename_machine_list

	   (concat m.mname.node_id i)

      if not (List.mem i reset_instances) then

	(* If not, declare mem_m = mem_c *)

	pp_no_reset machines m fmt i;

      let mems = full_memory_vars machines target_machine in

      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in

      let mid_mems = rename_mems rename_mid_list in

	fprintf fmt "@[<v 5>(and ";

	fprintf fmt "(= %a (ite %a %a %a))"

	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)

	  (pp_horn_val self (pp_horn_var m)) i1

	  (pp_horn_val self (pp_horn_var m)) i2

	;

	  (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)

	  (Utils.pp_final_char_if_non_empty "@ " outputs)

	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)

      end

    end

  with Not_found -> ( (* stateless node instance *)

      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))

      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)

  )

(* Print the instruction and update the set of reset instances *)

let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =

  match instr with

       statement. *)

    let self = m.mname.node_id in

    let pp_branch fmt (tag, instrs) =

	(*"@[<v 3>(=> (= %a %s)@ "*)  (* Issues with some versions of Z3. It

					  seems that => within Horn predicate

					  may cause trouble. I have hard time

      () (* rs *)

    in

    pp_conj pp_branch fmt hl;

  let ppi rs fmt i = pp_machine_instr machines rs m fmt i in

  match instrs with

  | _::_ ->

    fprintf fmt "(and @[<v 0>";

      let rs = ppi rs fmt i in

      fprintf fmt "@ ";

      rs

    )

    in

    fprintf fmt "@])";

    rs

  fprintf fmt "@[<v 5>(and @ ";

  (* print "x_m = x_c" for each local memory *)

    fprintf fmt "(= %a %a)"

      (pp_horn_var m) (rename_mid v)

      (pp_horn_var m) (rename_current v)

  *)

  (Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->

    let name = node_name n in

      fprintf fmt "(= %s._arrow._first_m true)"

    ) else (

	name

	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))

    )

   )) fmt m.minstances;

  else

    begin

      fprintf fmt "; %s@." m.mname.node_id;

      (* Printing variables *)

      Utils.fprintf_list ~sep:"@." pp_decl_var fmt

	(

	  (* Rule for reset *)

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

	    pp_machine_reset_name m.mname.node_id

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

		pp_machine_step_name m.mname.node_id

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

	    end

	    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 "; with Assertions @.";

	      (*Rule for step*)

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

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

		pp_machine_step_name m.mname.node_id

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

	    end

	end

    end

(* Local Variables: *)

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

(* End: *)

(* We extract the annotation dealing with traceability *)

  List.map (fun m ->

    let traces : (ident * expr) list=

      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in

    m, traces

  ) machines

let memories_old machines m =

  List.map (fun (p, v) ->

    let machine = match p with | [] -> m | (_,m')::_ -> m' in

    let traces = List.assoc machine (machines_traces machines) in

      (

	(* We take the expression associated to variable v in the trace

	   info *)

	   Printers.pp_expr (List.assoc v.var_id traces); *)

	p, List.assoc v.var_id traces

      )

      begin

	(* We keep the variable as is: we create an expression v *)

	(* eprintf "Unable to found variable %a in traces (%a)@."  pp_var v

	   (Utils.fprintf_list ~sep:", " pp_print_string) (List.map fst

	p, mkexpr Location.dummy_loc (Expr_ident v.var_id)

      end

  ) (compute_mems machines m)

let memories_next  machines m = (* We remove the topest pre in each expression *)

  List.map

    (fun (prefix, ee) ->

      	Printers.pp_expr ee;

      	assert false)

    (memories_old machines m)

let pp_prefix_rev fmt prefix =

    (List.rev prefix)

let traces_file fmt basename prog machines =

  fprintf fmt "<?xml version=\"1.0\"?>@.";

      let pp_var = pp_horn_var m in

      let memories_old = memories_old  machines m in

      let memories_next = memories_next  machines m in

      (* fprintf fmt "; Node %s@." m.mname.node_id; *)

      fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id;

      let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in

      let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in

      fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ "

	(Utils.fprintf_list ~sep:" | " pp_var)  output_vars

	(Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) output_vars

	(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);

      in

      let step_local_vars = (rename_current_list (full_memory_vars ~without_arrow:true machines m)) in

      fprintf fmt "@]@ </Node>";

     )) (List.rev machines);

  fprintf fmt "</Traces>@."

(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt

   "%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *)

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

open Utils

open LustreSpec

open Corelang

      close_in h_in;

      header

    with

      Parse.report_error err;

      raise exc

    | Corelang.Error (loc, err) as exc -> (

  Location.init lexbuf source_name;

  (* Parsing *)

    (fun fmt -> fprintf fmt ".. parsing source file %s@," source_name);

  try

    let prog = Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf in

    close_in s_in;

    prog

  with

    Parse.report_error err;

    raise exc

  | Corelang.Error (loc, err) as exc ->

      Location.pp_loc loc;

    raise exc

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

    begin

      try

	Typing.type_prog env decls

	  Types.pp_error err

	  Location.pp_loc loc;

	raise exc

  in

  if !Options.print_types then

    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_type decls);

  new_env

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

  let new_env =

    begin

let is_stateful topdecl =

  match topdecl.top_decl_desc with

  | Node nd -> (match nd.node_stateless with Some b -> not b | None -> not nd.node_dec_stateless)

  | _ -> false

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

    deps

  end

(* alias and type definition table *)

let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})

let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})

  "assumes", ASSUMES;

  "exists", EXISTS;

  "forall", FORALL;

  ]

}

  "assert", ASSERT;

  "lib", LIB;

  "prototype", PROTOTYPE;

]

    node_spec = None;

    node_annot = [];  }

  {

    top_decl_desc = Node arrow_desc;

    top_decl_owner = Version.include_path;

    top_decl_itf = false;

    top_decl_loc = Location.dummy_loc

  }

let mk_val v t = { value_desc = v; 

		   value_type = t; 

		   value_annot = None }

open Utils

open LustreSpec

open Compiler_common

exception StopPhase1 of program

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

  end

  match !Options.output with

  | "horn" | "lustre" | "acsl" -> true

  | _ -> false

(* From prog to prog *)

let stage1 prog dirname basename =

  let prog = expand_automata prog in

  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@.@[<v 2>@ %a@]@," Printers.pp_prog prog);

       exported as a lusi *)

    raise (StopPhase1 prog);

     - eliminate trivial expressions

 *)

  (*

    if !Options.const_unfold || !Options.optimization >= 5 then

      begin

	Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");