Project

General

Profile

Revision 86ae18b7

View differences:

README.md
1

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

  
4
[![Stories in Ready](https://badge.waffle.io/coco-team/lustrec.png?label=ready&title=Ready)](https://waffle.io/coco-team/lustrec)
5
[![Throughput Graph](https://graphs.waffle.io/coco-team/lustrec/throughput.svg)](https://waffle.io/coco-team/lustrec/metrics/throughput)
6

  
2 7
# LustreC
3 8

  
4 9
LustreC is a modular compiler of Lustre code into C and Horn Clauses.
configure.ac
1 1
define([gitversion], esyscmd([sh -c "git log --oneline | wc -l | tr -d '\n'"]))
2 2

  
3
AC_INIT([lustrec], [1.4-gitversion], [ploc@garoche.net])
4
AC_SUBST(VERSION_CODENAME, "Xia/Xiang-dev")
3
AC_INIT([lustrec], [1.3-gitversion], [ploc@garoche.net])
4
AC_SUBST(VERSION_CODENAME, "Xia/Zhong-Kang-dev")
5 5
# Next release will be
6
#AC_INIT([lustrec], [1.5], [ploc@garoche.net])
7
#AC_SUBST(VERSION_CODENAME, "Xia/Shao Kang")
6
#AC_INIT([lustrec], [1.3], [ploc@garoche.net])
7
#AC_SUBST(VERSION_CODENAME, "Xia/Zhong-Kang")
8

  
9
#AC_DEFINE(SVN_REVISION, "svnversion", [SVN Revision])
10
#AC_SUBST(SVN_REVISION)
8 11

  
9 12
AC_CONFIG_SRCDIR([src/main_lustre_compiler.ml])
10 13

  
......
98 101
# Instanciation
99 102
AC_CONFIG_FILES([Makefile
100 103
		 src/Makefile
101
                 src/myocamlbuild.ml
102 104
		 src/version.ml
103 105
		 test/test-compile.sh
104 106
		 ])
include/io_frontend.c
6 6
int ISATTY;
7 7

  
8 8
/* Standard Input procedures **************/
9
_Bool _get_bool(FILE* file, char* n){
9
_Bool _get_bool(char* n){
10 10
   char b[512];
11 11
   _Bool r = 0;
12 12
   int s = 1;
......
22 22
      if((c == '0') || (c == 'f') || (c == 'F')) r = 0;
23 23
      if((c == '1') || (c == 't') || (c == 'T')) r = 1;
24 24
   } while((s != 1) || (r == -1));
25
   fprintf(file, "%i\n",r);
26 25
   return r;
27 26
}
28

  
29
int _get_int(FILE* file, char* n){
27
int _get_int(char* n){
30 28
   char b[512];
31 29
   int r;
32 30
   int s = 1;
......
38 36
      if(scanf("%s", b)==EOF) exit(0);
39 37
      s = sscanf(b, "%d", &r);
40 38
   } while(s != 1);
41
   fprintf(file, "%d\n", r);
42 39
   return r;
43 40
}
44

  
45
double _get_double(FILE* file, char* n){
41
double _get_double(char* n){
46 42
   char b[512];
47 43
   double r;
48 44
   int s = 1;
......
54 50
      if(scanf("%s", b)==EOF) exit(0);
55 51
      s = sscanf(b, "%lf", &r);
56 52
   } while(s != 1);
57
   fprintf(file, "%f\n", r);
58 53
   return r;
59 54
}
60 55
/* Standard Output procedures **************/
61
void _put_bool(FILE* file, char* n, _Bool _V){
56
void _put_bool(char* n, _Bool _V){
62 57
  if(ISATTY) {
63 58
    printf("%s = ", n);
64 59
  } else {
......
66 61
  };
67 62
  printf("'%i' ", (_V)? 1 : 0);
68 63
  printf("\n");
69
  fprintf(file, "%i\n", _V);
70 64
}
71
void _put_int(FILE* file, char* n, int _V){
65
void _put_int(char* n, int _V){
72 66
  if(ISATTY) {
73 67
    printf("%s = ", n);
74 68
  } else {
......
76 70
  };
77 71
  printf("'%d' ", _V);
78 72
  printf("\n");
79
  fprintf(file, "%d\n", _V);
80 73
}
81
void _put_double(FILE* file, char* n, double _V){
74
void _put_double(char* n, double _V){
82 75
  if(ISATTY) {
83 76
    printf("%s = ", n);
84 77
  } else {
......
86 79
  };
87 80
  printf("'%f' ", _V);
88 81
  printf("\n");
89
  fprintf(file, "%f\n", _V);
90 82
}
include/io_frontend.h
7 7
/* Standard Input procedures **************/
8 8

  
9 9
/*@ assigns *n; */
10
extern _Bool _get_bool(FILE* file, char* n);
10
extern _Bool _get_bool(char* n);
11 11

  
12 12
/*@ assigns *n; */
13
extern int _get_int(FILE* file, char* n);
13
extern int _get_int(char* n);
14 14

  
15 15
/*@ assigns *n; */
16
extern double _get_double(FILE* file, char* n);
16
extern double _get_double(char* n);
17 17

  
18 18
/* Standard Output procedures **************/
19 19
/*@ assigns \nothing; */
20
extern void _put_bool(FILE* file, char* n, _Bool _V);
20
extern void _put_bool(char* n, _Bool _V);
21 21

  
22 22
/*@ assigns \nothing; */
23
extern void _put_int(FILE* file, char* n, int _V);
23
extern void _put_int(char* n, int _V);
24 24

  
25 25
/*@ assigns \nothing; */
26
extern void _put_double(FILE* file, char* n, double _V);
26
extern void _put_double(char* n, double _V);
27 27

  
28 28
#endif
include/math.smt2
1
(declare-rel  cbrt (Real Real))
2
(declare-rel  ceil (Real Real))
3
(declare-rel  erf (Real Real))
4
(declare-rel  fabs (Real Real))
5
(declare-rel  pow (Real Real Real))
6
(declare-rel  sqrt (Real Real))
lustrec.odocl
7 7
backends/C/C_backend_makefile
8 8
backends/C/C_backend_spec
9 9
backends/C/C_backend_src
10
backends/Horn/Horn_backend_common
11
backends/Horn/Horn_backend_printers
12
backends/Horn/Horn_backend_collecting_sem
13 10
backends/Horn/Horn_backend
14
plugins/scopes/Scopes
15 11
Basic_library
16 12
Causality
17 13
Clock_calculus
......
23 19
Delay_predef
24 20
Dimension
25 21
Env
26
Global
27 22
Inliner
28 23
Lexer_lustre
29 24
LexerLustreSpec
......
35 30
Machine_code
36 31
Main_lustre_compiler
37 32
Modules
38
Mpfr
39 33
Normalization
40 34
Optimize_machine
41 35
Optimize_prog
42 36
Options
43 37
Parse
44 38
Parser_lustre
45
Plugins
46 39
Printers
47 40
Scheduling
48 41
SortProg
share/FindLustre.cmake
17 17
#                  LUS_FILES <Lustre files>
18 18
#                  [USER_C_FILES <C files>]
19 19
#                  [VERBOSE <level>]
20
#                  [LUSI]
21 20
#                  LIBNAME <libraryName>)
22 21
#
23 22
# When used the Lustre_Compile macro define the variable
......
73 72
# Macros used to compile a lustre library
74 73
include(CMakeParseArguments)
75 74
function(Lustre_Compile)
76
  set(options LUSI)
75
  set(options "")
77 76
  set(oneValueArgs NODE LIBNAME VERBOSE)
78 77
  set(multiValueArgs LUS_FILES USER_C_FILES)
79 78
  cmake_parse_arguments(LUS "${options}" "${oneValueArgs}" "${multiValueArgs}" ${ARGN})
80 79

  
81
  if(LUS_LUSI)
82
    set(LUSTRE_LUSI_OPT "-lusi")
83
  endif()
84

  
85 80
  if (NOT LUS_LIBNAME)
86 81
    message(FATAL_ERROR "You should specify LIBNAME for each Lustre_Compile call.")
87 82
  endif()
88 83

  
89 84
  if(LUS_NODE)
90
    set(LUSTRE_NODE_OPT "-node;${LUS_NODE}")
85
    set(LUSTRE_NODE_OPT "-node ${LUS_NODE}")
91 86
    set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/lus_${LUS_LIBNAME}/${LUS_NODE}")
92 87
  else()
93 88
    set(LUSTRE_NODE_OPT "")
......
95 90
  endif()
96 91

  
97 92
  if (LUS_VERBOSE)
98
    set(LUSTRE_VERBOSE_OPT "-verbose;${LUS_VERBOSE}")
93
    set(LUSTRE_VERBOSE_OPT "-verbose ${LUS_VERBOSE}")
99 94
  else()
100 95
    # the default is to be quiet.
101 96
    set(LUSTRE_VERBOSE_OPT "-verbose;0")
......
110 105
    get_filename_component(E ${LFILE} EXT)
111 106
    if ("${E}" STREQUAL ".lus")
112 107
      set(LUSTRE_GENERATED_FILES ${LUSTRE_OUTPUT_DIR}/${L}.h ${LUSTRE_OUTPUT_DIR}/${L}.c ${LUSTRE_OUTPUT_DIR}/${L}_alloc.h)
113
      if(LUS_NODE)
114
         list(APPEND LUSTRE_GENERATED_FILES ${LUSTRE_OUTPUT_DIR}/${L}_main.c)
115
         list(APPEND LUSTRE_GENERATED_FILES ${LUSTRE_INCLUDE_DIR}/io_frontend.c)
116
      endif()
117 108
    elseif("${E}" STREQUAL ".lusi")
118 109
      set(LUSTRE_GENERATED_FILES ${LUSTRE_OUTPUT_DIR}/${L}.h)
119 110
    endif()
120 111
    list(APPEND GLOBAL_LUSTRE_GENERATED_C_FILES ${LUSTRE_GENERATED_FILES})
121 112
    set(LUSTRE_GENERATED_FILES ${LUSTRE_GENERATED_FILES} ${LUSTRE_OUTPUT_DIR}/${L}.lusic)
122
    if (LUS_LUSI)
123
      add_custom_command(
124
         OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/${LFILE}i
125
         COMMAND ${LUSTRE_COMPILER} ${LUSTRE_LUSI_OPT} ${LFILE}
126
         DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${LFILE}
127
         WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
128
         COMMENT "Compile Lustre source(s): ${LFILE} with option -lusi."
129
         )
130
      message(STATUS "lustrec will produce lusi file: ${LFILE}i")
131
    endif()
132 113
    add_custom_command(
133 114
      OUTPUT ${LUSTRE_GENERATED_FILES}
134 115
      COMMAND ${LUSTRE_COMPILER} ${LUSTRE_VERBOSE_OPT} ${LUSTRE_NODE_OPT} -d ${LUSTRE_OUTPUT_DIR} ${LFILE}
......
140 121
  endforeach()
141 122

  
142 123
  include_directories(${LUSTRE_INCLUDE_DIR} ${CMAKE_CURRENT_SOURCE_DIR} ${LUSTRE_OUTPUT_DIR})
143
  if(LUS_NODE)
144
  add_executable(${LUS_LIBNAME}
145
              ${GLOBAL_LUSTRE_GENERATED_C_FILES} ${LUS_USER_C_FILES}
146
              )
147
  else()
148 124
  add_library(${LUS_LIBNAME} SHARED
149 125
              ${GLOBAL_LUSTRE_GENERATED_C_FILES} ${LUS_USER_C_FILES}
150 126
              )
151
  endif()
152 127
  set_target_properties(${LUS_LIBNAME} PROPERTIES COMPILE_FLAGS "-std=c99")
153 128
  set(LUSTRE_GENERATED_C_FILES_${LUS_LIBNAME} "${GLOBAL_LUSTRE_GENERATED_C_FILES}" PARENT_SCOPE)
154 129
  message(STATUS "Lustre: Added rule for building lustre library: ${LUS_LIBNAME}")
src/_tags
2 2
"backends/Horn": include
3 3
<**/.svn>: -traverse
4 4
<**/.svn>: not_hygienic
5
"main_lustre_compiler.native": use_graph
5
#"main_lustre_compiler.native": package(ocamlgraph)
6 6
"main_lustre_compiler.native": use_str
7 7
"main_lustre_compiler.native": use_unix
8
<*.ml{,i}>: use_graph
8
#<*.ml{,i}>: package(ocamlgraph)
9 9
<*.ml{,i}>: use_str
10 10
<*.ml{,i}>: use_unix
src/backends/C/c_backend.ml
27 27

  
28 28
let gen_files funs basename prog machines dependencies =
29 29
  let destname = !Options.dest_dir ^ "/" ^ basename in
30
  
31
  let print_header, print_lib_c, print_main_c, print_makefile, print_cmake = funs in
30
  let source_main_file = destname ^ "_main.c" in (* Could be changed *)
31
  let makefile_file = destname ^ ".makefile" in (* Could be changed *)
32

  
33
  let print_header, print_lib_c, print_main_c, print_makefile = funs in
32 34

  
33 35
  (* Generating H file *)
34 36
  let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
......
36 38
  let header_fmt = formatter_of_out_channel header_out in
37 39
  print_header header_fmt basename prog machines dependencies;
38 40
  close_out header_out;
39
  
41

  
40 42
  (* Generating Lib C file *)
41 43
  let source_lib_file = destname ^ ".c" in (* Could be changed *)
42 44
  let source_lib_out = open_out source_lib_file in
......
44 46
  print_lib_c source_lib_fmt basename prog machines dependencies;
45 47
  close_out source_lib_out;
46 48

  
47
  (match !Options.main_node with
48
  | "" ->  () (* No main node: we do not generate main *)
49
  match !Options.main_node with
50
  | "" ->  () (* No main node: we do not generate main nor makefile *)
49 51
  | main_node -> (
50 52
    match Machine_code.get_machine_opt main_node machines with
51 53
    | None -> begin
......
54 56
      raise (Corelang.Error (Location.dummy_loc, LustreSpec.Main_not_found))
55 57
    end
56 58
    | Some m -> begin
57
      let source_main_file = destname ^ "_main.c" in (* Could be changed *)
58 59
      let source_main_out = open_out source_main_file in
59 60
      let source_main_fmt = formatter_of_out_channel source_main_out in
61
      let makefile_out = open_out makefile_file in
62
      let makefile_fmt = formatter_of_out_channel makefile_out in
60 63

  
61 64
      (* Generating Main C file *)
62 65
      print_main_c source_main_fmt m basename prog machines dependencies;
63 66

  
64
      close_out source_main_out;
67
      (* Generating Makefile *)
68
      print_makefile basename main_node dependencies makefile_fmt;
69

  
70
     close_out source_main_out;
71
     close_out makefile_out
72

  
65 73
    end
66
  ));
67

  
68

  
69
  (* Makefiles:
70
     - for the moment two cases
71
     1. Classical Makefile, only when provided with a main node
72
     May contain additional framac eacsl targets
73
     2. Cmake : 2 files
74
         - lustrec-basename.cmake describing all variables
75
         - the main CMakeLists.txt activating the first file
76
     - Later option 1 should be removed
77
  *)
78
  (* Case 1 *)
79
  (match !Options.main_node with
80
  | "" ->  () (* No main node: we do not generate main *)
81
  | main_node -> (
82
    let makefile_file = destname ^ ".makefile" in (* Could be changed *)
83
    let makefile_out = open_out makefile_file in
84
    let makefile_fmt = formatter_of_out_channel makefile_out in
85
    
86
    (* Generating Makefile *)
87
    print_makefile basename main_node dependencies makefile_fmt;
88
    
89
    close_out makefile_out
90
  ));
91
  
92
  (* Case 2 *)
93
  let cmake_file = "lustrec-" ^ basename ^ ".cmake" in
94
  let cmake_file_full_path = !Options.dest_dir ^ "/" ^ cmake_file in
95
  let cmake_out = open_out cmake_file_full_path in
96
  let cmake_fmt = formatter_of_out_channel cmake_out in
97
  (* Generating Makefile *)
98
  print_cmake basename main_node dependencies makefile_fmt;
99
    
100
    close_out makefile_out
101
  
74
  )
102 75

  
103 76
let translate_to_c basename prog machines dependencies =
104 77
  match !Options.spec with
......
112 85
    let module Source = C_backend_src.Main (SourceMod) in
113 86
    let module SourceMain = C_backend_main.Main (SourceMainMod) in
114 87
    let module Makefile = C_backend_makefile.Main (MakefileMod) in
115
    let module CMakefile = C_backend_cmake.Main (MakefileMod) in
116
    
117
    let funs = 
118
      Header.print_alloc_header, 
119
      Source.print_lib_c, 
120
      SourceMain.print_main_c, 
121
      Makefile.print_makefile,
122
      CMakefile.print_makefile
88

  
89
    let funs =
90
      Header.print_alloc_header,
91
      Source.print_lib_c,
92
      SourceMain.print_main_c,
93
      Makefile.print_makefile
123 94
    in
124
    gen_files funs basename prog machines dependencies 
95
    gen_files funs basename prog machines dependencies
125 96

  
126 97
  end
127 98
  | "acsl" -> begin
......
135 106
    let module Source = C_backend_src.Main (SourceMod) in
136 107
    let module SourceMain = C_backend_main.Main (SourceMainMod) in
137 108
    let module Makefile = C_backend_makefile.Main (MakefileMod) in
138
    let module CMakefile = C_backend_cmake.Main (MakefileMod) in
139
    
140
    let funs = 
141
      Header.print_alloc_header, 
109

  
110
    let funs =
111
      Header.print_alloc_header,
142 112
      Source.print_lib_c,
143 113
      SourceMain.print_main_c,
144
      Makefile.print_makefile,
145
      CMakefile.print_makefile 
114
      Makefile.print_makefile
146 115
    in
147
    gen_files funs basename prog machines dependencies 
116
    gen_files funs basename prog machines dependencies
148 117

  
149 118
  end
150 119
  | "c" -> begin
src/backends/C/c_backend_header.ml
39 39
      begin
40 40
	fprintf fmt "#include <mpfr.h>@."
41 41
      end;
42
    fprintf fmt "#include \"%s/arrow.h\"@.@." Version.include_path
42
(*fprintf fmt "#include \"%s/arrow.h\"@.@." Version.include_path*)
43
  fprintf fmt "#include \"%s/arrow.h\"@.@." !Options.include_dir
43 44
  end
44 45

  
45 46
let rec print_static_val pp_var fmt v =
src/backends/C/c_backend_main.ml
14 14
open Machine_code
15 15
open Format
16 16
open C_backend_common
17
open Utils
18 17

  
19 18
module type MODIFIERS_MAINSRC =
20 19
sig
......
32 31
(********************************************************************************************)
33 32

  
34 33
let print_get_inputs fmt m =
35
  let pi fmt (id, v', v) =
34
  let pi fmt (v', v) =
36 35
  match (Types.unclock_type v.var_type).Types.tdesc with
37
    | Types.Tint -> fprintf fmt "%s = _get_int(f_in%i, \"%s\")" v.var_id id v'.var_id
38
    | Types.Tbool -> fprintf fmt "%s = _get_bool(f_in%i, \"%s\")" v.var_id id v'.var_id
39
    | Types.Treal when !Options.mpfr -> fprintf fmt "mpfr_set_d(%s, _get_double(f_in%i, \"%s\"), %i)" v.var_id id v'.var_id (Mpfr.mpfr_prec ())
40
    | Types.Treal -> fprintf fmt "%s = _get_double(f_in%i, \"%s\")" v.var_id id v'.var_id
36
    | Types.Tint -> fprintf fmt "%s = _get_int(\"%s\")" v.var_id v'.var_id
37
    | Types.Tbool -> fprintf fmt "%s = _get_bool(\"%s\")" v.var_id v'.var_id
38
    | Types.Treal when !Options.mpfr -> fprintf fmt "mpfr_set_d(%s, _get_double(\"%s\"), %i)" v.var_id v'.var_id (Mpfr.mpfr_prec ())
39
    | Types.Treal -> fprintf fmt "%s = _get_double(\"%s\")" v.var_id v'.var_id
41 40
    | _ ->
42 41
      begin
43 42
	Global.main_node := !Options.main_node;
......
47 46
	raise (Error (v'.var_loc, Main_wrong_kind))
48 47
      end
49 48
  in
50
  List.iteri2 (fun idx v' v ->
51
    fprintf fmt "@ %a;" pi ((idx+1), v', v);
52
  ) m.mname.node_inputs m.mstep.step_inputs
49
  List.iter2 (fun v' v -> fprintf fmt "@ %a;" pi (v', v)) m.mname.node_inputs m.mstep.step_inputs
53 50

  
54 51
let print_put_outputs fmt m = 
55
  let po fmt (id, o', o) =
52
  let po fmt (o', o) =
56 53
    match (Types.unclock_type o.var_type).Types.tdesc with
57
    | Types.Tint -> fprintf fmt "_put_int(f_out%i, \"%s\", %s)" id o'.var_id o.var_id
58
    | Types.Tbool -> fprintf fmt "_put_bool(f_out%i, \"%s\", %s)" id o'.var_id o.var_id
59
    | Types.Treal when !Options.mpfr -> fprintf fmt "_put_double(f_out%i, \"%s\", mpfr_get_d(%s, %s))" id o'.var_id o.var_id (Mpfr.mpfr_rnd ())
60
    | Types.Treal -> fprintf fmt "_put_double(f_out%i, \"%s\", %s)" id o'.var_id o.var_id
54
    | Types.Tint -> fprintf fmt "_put_int(\"%s\", %s)" o'.var_id o.var_id
55
    | Types.Tbool -> fprintf fmt "_put_bool(\"%s\", %s)" o'.var_id o.var_id
56
    | Types.Treal when !Options.mpfr -> fprintf fmt "_put_double(\"%s\", mpfr_get_d(%s, %s))" o'.var_id o.var_id (Mpfr.mpfr_rnd ())
57
    | Types.Treal -> fprintf fmt "_put_double(\"%s\", %s)" o'.var_id o.var_id
61 58
    | _ -> assert false
62 59
  in
63
  Utils.List.iteri2 (fun idx v' v -> fprintf fmt "@ %a;" po ((idx+1), v', v)) m.mname.node_outputs m.mstep.step_outputs
60
  List.iter2 (fun v' v -> fprintf fmt "@ %a;" po (v', v)) m.mname.node_outputs m.mstep.step_outputs
61

  
62
let print_main_inout_declaration fmt m =
63
  begin
64
    fprintf fmt "/* Declaration of inputs/outputs variables */@ ";
65
    List.iter 
66
      (fun v -> fprintf fmt "%a;@ " (pp_c_type v.var_id) v.var_type
67
      ) m.mstep.step_inputs;
68
    List.iter 
69
      (fun v -> fprintf fmt "%a;@ " (pp_c_type v.var_id) v.var_type
70
      ) m.mstep.step_outputs
71
  end
64 72

  
65
let print_main_inout_declaration basename fmt m =
66
  let mname = m.mname.node_id in
67
  fprintf fmt "/* Declaration of inputs/outputs variables */@ ";
68
  List.iteri 
69
    (fun idx v ->
70
      fprintf fmt "%a;@ " (pp_c_type v.var_id) v.var_type;
71
      fprintf fmt "FILE *f_in%i;@ " (idx+1); (* we start from 1: in1, in2, ... *)
72
      fprintf fmt "f_in%i = fopen(\"%s_%s_simu.in%i\", \"w\");@ " (idx+1) basename mname (idx+1);
73
    ) m.mstep.step_inputs;
74
  List.iteri 
75
    (fun idx v ->
76
      fprintf fmt "%a;@ " (pp_c_type v.var_id) v.var_type;
77
      fprintf fmt "FILE *f_out%i;@ " (idx+1); (* we start from 1: in1, in2, ... *)
78
      fprintf fmt "f_out%i = fopen(\"%s_%s_simu.out%i\", \"w\");@ " (idx+1) basename mname (idx+1);
79
    ) m.mstep.step_outputs
80

  
81

  
82
  
83 73
let print_main_memory_allocation mname main_mem fmt m =
84 74
  if not (fst (get_stateless_status m)) then
85 75
  begin  
......
142 132
    fprintf fmt "@ /* Infinite loop */@ ";
143 133
    fprintf fmt "@[<v 2>while(1){@ ";
144 134
    fprintf fmt  "fflush(stdout);@ ";
145
    List.iteri (fun idx _ -> fprintf fmt "fflush(f_in%i);@ " (idx+1)) m.mstep.step_inputs;
146
    List.iteri (fun idx _ -> fprintf fmt "fflush(f_out%i);@ " (idx+1)) m.mstep.step_outputs;
147 135
    fprintf fmt "%a@ %t%a"
148 136
      print_get_inputs m
149 137
      (fun fmt -> pp_main_call mname main_mem fmt m input_values m.mstep.step_outputs)
......
157 145
    then "&main_mem"
158 146
    else "main_mem" in
159 147
  fprintf fmt "@[<v 2>int main (int argc, char *argv[]) {@ ";
160
  print_main_inout_declaration basename fmt m;
148
  print_main_inout_declaration fmt m;
161 149
  print_main_memory_allocation mname main_mem fmt m;
162 150
  if !Options.mpfr then
163 151
    begin
......
179 167
  fprintf fmt "@]@ }@."       
180 168

  
181 169
let print_main_header fmt =
182
  fprintf fmt "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.h\"@." Version.include_path 
170
(*fprintf fmt "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.h\"@." Version.include_path*)
171
fprintf fmt "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.h\"@." !Options.include_dir
183 172

  
184 173

  
185 174
let print_main_c main_fmt main_machine basename prog machines _ (*dependencies*) =
src/backends/Horn/horn_backend.ml
48 48
    )
49 49
end
50 50

  
51

  
52
let load_file f =
53
  let ic = open_in f in
54
  let n = in_channel_length ic in
55
  let s = String.create n in
56
  really_input ic s 0 n;
57
  close_in ic;
58
  (s)
59

  
51 60
let print_type_definitions fmt =
52 61
  let cpt_type = ref 0 in
53 62
  Hashtbl.iter (fun typ decl ->
......
68 77
    | _        -> ()) type_table
69 78

  
70 79

  
71
let translate fmt basename prog machines =
80

  
81

  
82
let print_dep fmt prog =
83
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting Horn libraries@,");
84
  fprintf fmt "; Statically linked libraries@";
85
  let dependencies = Corelang.get_dependencies prog in
86
  List.iter
87
    (fun dep ->
88
      let (local, s) = Corelang.dependency_of_top dep in
89
      let basename = ((if local then !Options.dest_dir else !Options.include_dir)) ^ s ^ ".smt2" in
90
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0> Horn Library %s@," basename);
91
      let horn = load_file basename in
92
      fprintf fmt "@.%s@." horn;
93
    )
94
    dependencies
95

  
96
let check_sfunction mannot =
97
 (*Check if its an sfunction*)
98
  match mannot with
99
    [] -> false
100
  | [x] ->
101
     begin
102
       match x.annots with
103
         [] -> false
104
        |[(key,va)] ->
105
          begin
106
            match key with
107
              [] -> false
108
            | [x]  -> x == "c_code" || x =="matlab"
109
            | _ -> false
110
          end
111
        |(_,_)::_ -> false
112
     end
113
  | _::_ -> false
114

  
115
let translate fmt basename prog machines=
72 116
  (* We print typedef *)
117
  print_dep fmt prog; (*print static library e.g. math*)
73 118
  print_type_definitions fmt;
74
  List.iter (print_machine machines fmt) (List.rev machines);
119
  (*List.iter (print_machine machines fmt) (List.rev machines);*)
120
  List.iter(fun m ->
121
      let is_sfunction = check_sfunction m.mannot in
122
      if is_sfunction then(
123
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. detected sfunction: %s@," m.mname.node_id);
124
        print_sfunction machines fmt m
125
      ) else (
126
         print_machine machines fmt m)
127
         )
128
           (List.rev machines);
75 129
  main_print machines fmt
76 130

  
77 131
(* Local Variables: *)
src/backends/Horn/horn_backend_common.ml
25 25
  | Types.Treal           -> fprintf fmt "Real"
26 26
  | Types.Tconst ty       -> pp_print_string fmt ty
27 27
  | Types.Tclock t        -> pp_type fmt t
28
  | Types.Tarray _
29
  | Types.Tstatic _
28
  | Types.Tarray(dim,ty)   -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")"
29
  | Types.Tstatic(d, ty)-> pp_type fmt ty
30 30
  | Types.Tarrow _
31 31
  | _                     -> eprintf "internal error: pp_type %a@."
32 32
    Types.print_ty t; assert false
......
69 69

  
70 70
let local_memory_vars machines machine =
71 71
  rename_machine_list machine.mname.node_id machine.mmemory
72
    
72

  
73 73
let instances_memory_vars ?(without_arrow=false) machines machine =
74 74
  let rec aux fst prefix m =
75 75
    (
......
81 81
      List.fold_left (fun accu (id, (n, _)) ->
82 82
	let name = node_name n in
83 83
	if without_arrow && name = "_arrow" then
84
	  accu 
84
	  accu
85 85
	else
86 86
	  let machine_n = get_machine machines name in
87
	  ( aux false (concat prefix 
87
	  ( aux false (concat prefix
88 88
			 (if fst then id else concat m.mname.node_id id))
89 89
	      machine_n ) @ accu
90 90
      ) [] (m.minstances)
......
101 101

  
102 102
let step_vars machines m =
103 103
  (inout_vars machines m)
104
  @ (rename_current_list (full_memory_vars machines m)) 
104
  @ (rename_current_list (full_memory_vars machines m))
105 105
  @ (rename_next_list (full_memory_vars machines m))
106 106

  
107 107
let step_vars_m_x machines m =
108 108
  (inout_vars machines m)
109
  @ (rename_mid_list (full_memory_vars machines m)) 
109
  @ (rename_mid_list (full_memory_vars machines m))
110 110
  @ (rename_next_list (full_memory_vars machines m))
111 111

  
112 112
let reset_vars machines m =
113
  (rename_current_list (full_memory_vars machines m)) 
113
  (rename_current_list (full_memory_vars machines m))
114 114
  @ (rename_mid_list (full_memory_vars machines m))
115 115

  
116 116

  
src/backends/Horn/horn_backend_printers.ml
21 21
open Machine_code
22 22

  
23 23
open Horn_backend_common
24

  
24
open Types
25 25

  
26 26
(********************************************************************************************)
27 27
(*                    Instruction Printing functions                                        *)
28 28
(********************************************************************************************)
29 29

  
30 30
let pp_horn_var m fmt id =
31
  if Types.is_array_type id.var_type
31
  (*if Types.is_array_type id.var_type
32 32
  then
33 33
    assert false (* no arrays in Horn output *)
34
  else
34
  else*)
35 35
    fprintf fmt "%s" id.var_id
36 36

  
37 37
(* Used to print boolean constants *)
......
46 46
    | Const_tag t    -> pp_horn_tag fmt t
47 47
    | _              -> assert false
48 48

  
49
(* PL comment 2017/01/03: Useless code, the function existed before in typing.ml *)
50
(* let rec get_type_cst c = *)
51
(*   match c with *)
52
(*   | Const_int(n) -> new_ty Tint *)
53
(*   | Const_real _ -> new_ty Treal *)
54
(*   (\* | Const_float _ -> new_ty Treal *\) *)
55
(*   | Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), *)
56
(* 				     get_type_cst (List.hd l))) *)
57
(*   | Const_tag(tag) -> new_ty Tbool *)
58
(*   | Const_string(str) ->  assert false(\* used only for annotations *\) *)
59
(*   | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l)) *)
60

  
61
(* PL comment 2017/01/03: the following function get_type seems useless to me: it looks like computing the type of a machine code expression v while v.value_type should contain this information. The code is kept for the moment in case I missed something *)
62

  
63
(*
64
let rec get_type v =
65
  match v with
66
  | Cst c -> Typing.type_const Location.dummy_loc c (* get_type_cst c*)
67
  | Access(tab, index) -> begin
68
      let rec remove_link ltype =
69
        match (dynamic_type ltype).tdesc with
70
        | Tlink t -> t
71
        | _ -> ltype
72
      in
73
      match (dynamic_type (remove_link (get_type tab))).tdesc with
74
      | Tarray(size, t) -> remove_link t
75
      | Tvar -> Format.eprintf "Type of access is a variable... "; assert false
76
      | Tunivar -> Format.eprintf "Type of access is a variable... "; assert false
77
      | _ -> Format.eprintf "Type of access is not an array "; assert false
78
                          end
79
  | Power(v, n) -> assert false
80
  | LocalVar v -> v.var_type
81
  | StateVar v -> v.var_type
82
  | Fun(n, vl) -> begin match n with
83
                  | "+"
84
                  | "-"
85
                  | "*" -> get_type (List.hd vl)
86
                  | _ -> Format.eprintf "Function undealt with : %s" n ;assert false
87
                  end
88
  | Array(l) -> new_ty (Tarray(Dimension.mkdim_int
89
                                 (Location.dummy_loc)
90
                                 (List.length l),
91
                               get_type (List.hd l)))
92
  | _ -> assert false
93
*)
94

  
95
(* Default value for each type, used when building arrays. Eg integer array
96
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
97
   for the type integer (arrays).
98
*)
99
let rec pp_default_val fmt t =
100
  match (dynamic_type t).tdesc with
101
  | Tint -> fprintf fmt "0"
102
  | Treal -> fprintf fmt "0"
103
  | Tbool -> fprintf fmt "true"
104
  | Tarray(dim, l) -> (* TODO PL: this strange code has to be (heavily) checked *)
105
     let valt = array_element_type t in
106
     fprintf fmt "((as const (Array Int %a)) %a)"
107
       pp_type valt 
108
       pp_default_val valt
109
  | Tstruct(l) -> assert false
110
  | Ttuple(l) -> assert false
111
  |_ -> assert false
112

  
113

  
49 114
(* Prints a value expression [v], with internal function calls only.
50 115
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
51 116
   but an offset suffix may be added for array variables
52 117
*)
53 118
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
54 119
  match v.value_desc with
55
    | Cst c         -> pp_horn_const fmt c
56
    | Array _
57
    | Access _ -> assert false (* no arrays *)
58
    | Power (v, n)  -> assert false
59
    | LocalVar v    -> pp_var fmt (rename_machine self v)
60
    | StateVar v    ->
61
      if Types.is_array_type v.var_type
62
      then assert false
63
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
64
    | Fun (n, vl)   -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
120
  | Cst c       -> pp_horn_const fmt c
121

  
122
  (* Code specific for arrays *)
123
  | Array il    ->
124
     (* An array definition: 
125
	(store (
126
	  ...
127
 	    (store (
128
	       store (
129
	          default_val
130
	       ) 
131
	       idx_n val_n
132
	    ) 
133
	    idx_n-1 val_n-1)
134
	  ... 
135
	  idx_1 val_1
136
	) *)
137
     let rec print fmt (tab, x) =
138
       match tab with
139
       | [] -> pp_default_val fmt v.value_type(* (get_type v) *)
140
       | h::t ->
141
	  fprintf fmt "(store %a %i %a)"
142
	    print (t, (x+1))
143
	    x
144
	    (pp_horn_val ~is_lhs:is_lhs self pp_var) h
145
     in
146
     print fmt (il, 0)
147
       
148
  | Access(tab,index) ->
149
     fprintf fmt "(select %a %a)"
150
       (pp_horn_val ~is_lhs:is_lhs self pp_var) tab
151
       (pp_horn_val ~is_lhs:is_lhs self pp_var) index
152

  
153
  (* Code specific for arrays *)
154
    
155
  | Power (v, n)  -> assert false
156
  | LocalVar v    -> pp_var fmt (rename_machine self v)
157
  | StateVar v    ->
158
     if Types.is_array_type v.var_type
159
     then assert false
160
     else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
161
  | Fun (n, vl)   -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
65 162

  
66 163
(* Prints a [value] indexed by the suffix list [loop_vars] *)
67 164
let rec pp_value_suffix self pp_value fmt value =
......
79 176
*)
80 177
let pp_assign m pp_var fmt var_name value =
81 178
  let self = m.mname.node_id in
82
  fprintf fmt "(= %a %a)" 
179
  fprintf fmt "(= %a %a)"
83 180
    (pp_horn_val ~is_lhs:true self pp_var) var_name
84 181
    (pp_value_suffix self pp_var) value
85
    
182

  
86 183

  
87 184
(* In case of no reset call, we define mid_mem = current_mem *)
88 185
let pp_no_reset machines m fmt i =
89 186
  let (n,_) = List.assoc i m.minstances in
90 187
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
91 188

  
92
  let m_list = 
189
  let m_list =
93 190
    rename_machine_list
94 191
      (concat m.mname.node_id i)
95 192
      (rename_mid_list (full_memory_vars machines target_machine))
......
104 201
    fprintf fmt "(= %a %a)"
105 202
      (pp_horn_var m) mhd
106 203
      (pp_horn_var m) chd
107
  
204

  
108 205
  | _ -> (
109 206
    fprintf fmt "@[<v 0>(and @[<v 0>";
110
    List.iter2 (fun mhd chd -> 
207
    List.iter2 (fun mhd chd ->
111 208
      fprintf fmt "(= %a %a)@ "
112 209
      (pp_horn_var m) mhd
113 210
      (pp_horn_var m) chd
......
120 217
let pp_instance_reset machines m fmt i =
121 218
  let (n,_) = List.assoc i m.minstances in
122 219
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
123
  
220

  
124 221
  fprintf fmt "(%a @[<v 0>%a)@]"
125 222
    pp_machine_reset_name (node_name n)
126
    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
223
    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
127 224
    (
128 225
      (rename_machine_list
129 226
	 (concat m.mname.node_id i)
130 227
	 (rename_current_list (full_memory_vars machines target_machine))
131
      ) 
228
      )
132 229
      @
133 230
	(rename_machine_list
134 231
	   (concat m.mname.node_id i)
......
146 243
      if not (List.mem i reset_instances) then
147 244
	(* If not, declare mem_m = mem_c *)
148 245
	pp_no_reset machines m fmt i;
149
      
246

  
150 247
      let mems = full_memory_vars machines target_machine in
151 248
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
152 249
      let mid_mems = rename_mems rename_mid_list in
......
157 254
	fprintf fmt "@[<v 5>(and ";
158 255
	fprintf fmt "(= %a (ite %a %a %a))"
159 256
	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
160
	  (pp_horn_var m) mem_m 
257
	  (pp_horn_var m) mem_m
161 258
	  (pp_horn_val self (pp_horn_var m)) i1
162 259
	  (pp_horn_val self (pp_horn_var m)) i2
163 260
	;
......
175 272
	  (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
176 273
	  (Utils.pp_final_char_if_non_empty "@ " outputs)
177 274
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
178
	
275

  
179 276
      end
180 277
    end
181 278
  with Not_found -> ( (* stateless node instance *)
......
188 285
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
189 286
      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
190 287
  )
191
    
192
    
288

  
289

  
193 290
(* Print the instruction and update the set of reset instances *)
194 291
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
195 292
  match instr with
......
230 327
       statement. *)
231 328
    let self = m.mname.node_id in
232 329
    let pp_branch fmt (tag, instrs) =
233
      fprintf fmt 
234
	"@[<v 3>(or (not (= %a %s))@ " 
330
      fprintf fmt
331
	"@[<v 3>(or (not (= %a %s))@ "
235 332
	(*"@[<v 3>(=> (= %a %s)@ "*)  (* Issues with some versions of Z3. It
236 333
					  seems that => within Horn predicate
237 334
					  may cause trouble. I have hard time
......
244 341
      () (* rs *)
245 342
    in
246 343
    pp_conj pp_branch fmt hl;
247
    reset_instances 
344
    reset_instances
248 345

  
249
and pp_machine_instrs machines reset_instances m fmt instrs = 
346
and pp_machine_instrs machines reset_instances m fmt instrs =
250 347
  let ppi rs fmt i = pp_machine_instr machines rs m fmt i in
251 348
  match instrs with
252
  | [x] -> ppi reset_instances fmt x 
349
  | [x] -> ppi reset_instances fmt x
253 350
  | _::_ ->
254 351
    fprintf fmt "(and @[<v 0>";
255
    let rs = List.fold_left (fun rs i -> 
352
    let rs = List.fold_left (fun rs i ->
256 353
      let rs = ppi rs fmt i in
257 354
      fprintf fmt "@ ";
258 355
      rs
259 356
    )
260
      reset_instances instrs 
357
      reset_instances instrs
261 358
    in
262 359
    fprintf fmt "@])";
263 360
    rs
......
269 366
  fprintf fmt "@[<v 5>(and @ ";
270 367

  
271 368
  (* print "x_m = x_c" for each local memory *)
272
  (Utils.fprintf_list ~sep:"@ " (fun fmt v -> 
369
  (Utils.fprintf_list ~sep:"@ " (fun fmt v ->
273 370
    fprintf fmt "(= %a %a)"
274 371
      (pp_horn_var m) (rename_mid v)
275 372
      (pp_horn_var m) (rename_current v)
......
281 378
  *)
282 379
  (Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->
283 380
    let name = node_name n in
284
    if name = "_arrow" then ( 
381
    if name = "_arrow" then (
285 382
      fprintf fmt "(= %s._arrow._first_m true)"
286
	(concat m.mname.node_id id)  
383
	(concat m.mname.node_id id)
287 384
    ) else (
288
      let machine_n = get_machine machines name in 
289
      fprintf fmt "(%s_reset @[<hov 0>%a@])" 
385
      let machine_n = get_machine machines name in
386
      fprintf fmt "(%s_reset @[<hov 0>%a@])"
290 387
	name
291
	(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
388
	(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
292 389
	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
293 390
    )
294 391
   )) fmt m.minstances;
......
314 411
  else
315 412
    begin
316 413
      fprintf fmt "; %s@." m.mname.node_id;
317
      
414

  
318 415
      (* Printing variables *)
319 416
      Utils.fprintf_list ~sep:"@." pp_decl_var fmt
320 417
	(
......
358 455

  
359 456
	  (* Rule for reset *)
360 457
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
361
	    (pp_machine_reset machines) m 
458
	    (pp_machine_reset machines) m
362 459
	    pp_machine_reset_name m.mname.node_id
363 460
	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
364 461

  
......
373 470
		pp_machine_step_name m.mname.node_id
374 471
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
375 472
	    end
376
	  | assertsl -> 
473
	  | assertsl ->
377 474
	    begin
378 475
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
379 476
	      (* print_string pp_val; *)
380 477
	      fprintf fmt "; with Assertions @.";
381
	      
478

  
382 479
	      (*Rule for step*)
383 480
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
384 481
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
......
386 483
		pp_machine_step_name m.mname.node_id
387 484
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
388 485
	    end
389
	      
390
	      
486

  
487

  
391 488
	end
392 489
    end
393 490

  
394 491

  
492
let mk_flags arity =
493
  let b_range =
494
   let rec range i j =
495
     if i > arity then [] else i :: (range (i+1) j) in
496
   range 2 arity;
497
 in
498
 List.fold_left (fun acc x -> acc ^ " false") "true" b_range
499

  
500

  
501
  (*Get sfunction infos from command line*)
502
let get_sf_info() =
503
  let splitted = Str.split (Str.regexp "@") !Options.sfunction in
504
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. sfunction name: %s@," !Options.sfunction);
505
  let sf_name, flags, arity = match splitted with
506
      [h;flg;par] -> h, flg, par
507
    | _ -> failwith "Wrong Sfunction info"
508

  
509
  in
510
  Log.report ~level:1 (fun fmt -> fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags arity);
511
  sf_name, flags, arity
512

  
513

  
514
    (*a function to print the rules in case we have an s-function*)
515
  let print_sfunction machines fmt m =
516
      if m.mname.node_id = arrow_id then
517
        (* We don't print arrow function *)
518
        ()
519
      else
520
        begin
521
          Format.fprintf fmt "; SFUNCTION@.";
522
          Format.fprintf fmt "; %s@." m.mname.node_id;
523
          Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction;
524

  
525
          (* Check if there is annotation for s-function *)
526
          if m.mannot != [] then(
527
              Format.fprintf fmt "; @[%a@]@]@\n" (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) m.mannot;
528
            );
529

  
530
       (* Printing variables *)
531
          Utils.fprintf_list ~sep:"@." pp_decl_var fmt
532
                             ((step_vars machines m)@
533
    	                        (rename_machine_list m.mname.node_id m.mstep.step_locals));
534
          Format.pp_print_newline fmt ();
535
          let sf_name, flags, arity = get_sf_info() in
536

  
537
       if is_stateless m then
538
         begin
539
           (* Declaring single predicate *)
540
           Format.fprintf fmt "(declare-rel %a (%a))@."
541
    	                  pp_machine_stateless_name m.mname.node_id
542
    	                  (Utils.fprintf_list ~sep:" " pp_type)
543
    	                  (List.map (fun v -> v.var_type) (reset_vars machines m));
544
           Format.pp_print_newline fmt ();
545
           (* Rule for single predicate *)
546
           let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in
547
           Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@."
548
                          str_flags
549
                          (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m)
550
	                  pp_machine_stateless_name m.mname.node_id
551
	                  (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m);
552
         end
553
      else
554
         begin
555
           (* Declaring predicate *)
556
           Format.fprintf fmt "(declare-rel %a (%a))@."
557
    	                  pp_machine_reset_name m.mname.node_id
558
    	                  (Utils.fprintf_list ~sep:" " pp_type)
559
    	                  (List.map (fun v -> v.var_type) (inout_vars machines m));
560

  
561
           Format.fprintf fmt "(declare-rel %a (%a))@."
562
    	                  pp_machine_step_name m.mname.node_id
563
    	                  (Utils.fprintf_list ~sep:" " pp_type)
564
    	                  (List.map (fun v -> v.var_type) (step_vars machines m));
565

  
566
           Format.pp_print_newline fmt ();
567
          (* Adding assertions *)
568
           match m.mstep.step_asserts with
569
	  | [] ->
570
	    begin
571

  
572
	      (* Rule for step*)
573
	      fprintf fmt "@[<v 2>(rule (=> @ ";
574
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
575
	      fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
576
		pp_machine_step_name m.mname.node_id
577
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
578
	    end
579
	  | assertsl ->
580
	    begin
581
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
582
	      (* print_string pp_val; *)
583
	      fprintf fmt "; with Assertions @.";
584

  
585
	      (*Rule for step*)
586
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
587
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
588
	      fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
589
		pp_machine_step_name m.mname.node_id
590
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
591
	    end
592

  
593
         end
594

  
595
        end
395 596
(* Local Variables: *)
396 597
(* compile-command:"make -C ../../.." *)
397 598
(* End: *)
src/backends/Horn/horn_backend_traces.ml
39 39

  
40 40

  
41 41
(* We extract the annotation dealing with traceability *)
42
let machines_traces machines = 
42
let machines_traces machines =
43 43
  List.map (fun m ->
44 44
    let traces : (ident * expr) list=
45 45
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
......
61 61
    m, traces
62 62

  
63 63
  ) machines
64
  
64

  
65 65
let memories_old machines m =
66 66
  List.map (fun (p, v) ->
67 67
    let machine = match p with | [] -> m | (_,m')::_ -> m' in
68 68
    let traces = List.assoc machine (machines_traces machines) in
69
    if List.mem_assoc v.var_id traces then 
69
    if List.mem_assoc v.var_id traces then
70 70
      (
71 71
	(* We take the expression associated to variable v in the trace
72 72
	   info *)
......
75 75
	   Printers.pp_expr (List.assoc v.var_id traces); *)
76 76
	p, List.assoc v.var_id traces
77 77
      )
78
    else 
78
    else
79 79
      begin
80 80

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

  
83 83
	(* eprintf "Unable to found variable %a in traces (%a)@."  pp_var v
84 84
	   (Utils.fprintf_list ~sep:", " pp_print_string) (List.map fst
85
	   traces); *)	    
85
	   traces); *)
86 86

  
87 87
	p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
88 88
      end
89 89

  
90 90
  ) (compute_mems machines m)
91
      
91

  
92 92
let memories_next  machines m = (* We remove the topest pre in each expression *)
93 93
  List.map
94 94
    (fun (prefix, ee) ->
......
102 102
      	Printers.pp_expr ee;
103 103
      	assert false)
104 104
    (memories_old machines m)
105
      
105

  
106 106

  
107 107

  
108 108
let pp_prefix_rev fmt prefix =
109
  Utils.fprintf_list ~sep:"." 
110
    (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) 
111
    fmt 
109
  Utils.fprintf_list ~sep:"."
110
    (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id)
111
    fmt
112 112
    (List.rev prefix)
113
      
113

  
114 114

  
115 115
let traces_file fmt basename prog machines =
116 116
  fprintf fmt "<?xml version=\"1.0\"?>@.";
......
120 120
      let pp_var = pp_horn_var m in
121 121
      let memories_old = memories_old  machines m in
122 122
      let memories_next = memories_next  machines m in
123
      
123

  
124 124
      (* fprintf fmt "; Node %s@." m.mname.node_id; *)
125 125
      fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id;
126
      
126

  
127 127
      let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in
128 128
      let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in
129 129
      fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ "
......
135 135
	(Utils.fprintf_list ~sep:" | " pp_var)  output_vars
136 136
	(Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) output_vars
137 137
	(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);
138
      
139
      let init_local_vars = 
140
	
141
	  (rename_next_list (try full_memory_vars ~without_arrow:true machines m with Not_found -> Format.eprintf "mahine %s@.@?" m.mname.node_id; assert false)) 
142
	
138

  
139
      let init_local_vars =
140
	(rename_next_list
141
           (try full_memory_vars ~without_arrow:true machines m with Not_found -> Format.eprintf "mahine %s@.@?" m.mname.node_id; assert false))
142

  
143 143

  
144 144
      in
145 145
      let step_local_vars = (rename_current_list (full_memory_vars ~without_arrow:true machines m)) in
......
160 160
      fprintf fmt "@]@ </Node>";
161 161
     )) (List.rev machines);
162 162
  fprintf fmt "</Traces>@."
163
  
163

  
164 164

  
165 165
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt
166 166
   "%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *)
src/compiler_common.ml
10 10
(********************************************************************)
11 11

  
12 12
open Utils
13
open Format 
13
open Format
14 14
open LustreSpec
15 15
open Corelang
16 16

  
......
50 50
      close_in h_in;
51 51
      header
52 52
    with
53
    | (Parse.Error err) as exc -> 
53
    | (Parse.Error err) as exc ->
54 54
      Parse.report_error err;
55 55
      raise exc
56 56
    | Corelang.Error (loc, err) as exc -> (
......
68 68
  Location.init lexbuf source_name;
69 69

  
70 70
  (* Parsing *)
71
  Log.report ~level:1 
71
  Log.report ~level:1
72 72
    (fun fmt -> fprintf fmt ".. parsing source file %s@," source_name);
73 73
  try
74 74
    let prog = Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf in
......
76 76
    close_in s_in;
77 77
    prog
78 78
  with
79
  | (Parse.Error err) as exc -> 
79
  | (Parse.Error err) as exc ->
80 80
    Parse.report_error err;
81 81
    raise exc
82 82
  | Corelang.Error (loc, err) as exc ->
......
115 115
      Location.pp_loc loc;
116 116
    raise exc
117 117

  
118
let type_decls env decls =  
118
let type_decls env decls =
119 119
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. typing@ ");
120
  let new_env = 
120
  let new_env =
121 121
    begin
122 122
      try
123 123
	Typing.type_prog env decls
......
126 126
	  Types.pp_error err
127 127
	  Location.pp_loc loc;
128 128
	raise exc
129
    end 
129
    end
130 130
  in
131 131
  if !Options.print_types then
132 132
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_type decls);
133 133
  new_env
134
      
135
let clock_decls env decls = 
134

  
135
let clock_decls env decls =
136 136
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@ ");
137 137
  let new_env =
138 138
    begin
......
221 221
let is_stateful topdecl =
222 222
  match topdecl.top_decl_desc with
223 223
  | Node nd -> (match nd.node_stateless with Some b -> not b | None -> not nd.node_dec_stateless)
224
  | ImportedNode nd -> not nd.nodei_stateless 
224
  | ImportedNode nd -> not nd.nodei_stateless
225 225
  | _ -> false
226 226

  
227 227

  
......
248 248
    Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
249 249
    deps
250 250
  end
251

  
src/corelang.ml
241 241

  
242 242
(* alias and type definition table *)
243 243

  
244
let mktop = mktop_decl Location.dummy_loc Version.include_path false 
244
(*let mktop = mktop_decl Location.dummy_loc Version.include_path false *)
245

  
246
let mktop = mktop_decl Location.dummy_loc !Options.include_dir false
245 247

  
246 248
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})
247 249
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})
src/lexerLustreSpec.mll
66 66
  "assumes", ASSUMES;
67 67
  "exists", EXISTS;
68 68
  "forall", FORALL;
69
  "c_code", CCODE;
70
  "matlab", MATLAB;
69 71
  ]
70 72

  
71 73
}
src/lexer_lustre.mll
63 63
  "assert", ASSERT;
64 64
  "lib", LIB;
65 65
  "prototype", PROTOTYPE;
66
  "c_code", CCODE;
67
  "matlab", MATLAB;
66 68
]
67 69

  
68 70

  
src/machine_code.ml
161 161
    node_spec = None;
162 162
    node_annot = [];  }
163 163

  
164
let arrow_top_decl =
164
(*let arrow_top_decl =
165 165
  {
166 166
    top_decl_desc = Node arrow_desc;
167 167
    top_decl_owner = Version.include_path;
168 168
    top_decl_itf = false;
169 169
    top_decl_loc = Location.dummy_loc
170
  }*)
171

  
172
let arrow_top_decl =
173
  {
174
    top_decl_desc = Node arrow_desc;
175
    top_decl_owner = !Options.include_dir;
176
    top_decl_itf = false;
177
    top_decl_loc = Location.dummy_loc
170 178
  }
171 179

  
180

  
172 181
let mk_val v t = { value_desc = v; 
173 182
		   value_type = t; 
174 183
		   value_annot = None }
src/main_lustre_compiler.ml
15 15
open Utils
16 16
open LustreSpec
17 17
open Compiler_common
18
 
18

  
19 19
exception StopPhase1 of program
20 20

  
21 21
let usage = "Usage: lustrec [options] \x1b[4msource file\x1b[0m"
......
88 88
  end
89 89

  
90 90

  
91
let functional_backend () = 
91
let functional_backend () =
92 92
  match !Options.output with
93 93
  | "horn" | "lustre" | "acsl" -> true
94 94
  | _ -> false
95 95

  
96 96
(* From prog to prog *)
97 97
let stage1 prog dirname basename =
98
  (* Removing automata *) 
98
  (* Removing automata *)
99 99
  let prog = expand_automata prog in
100 100

  
101 101
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@.@[<v 2>@ %a@]@," Printers.pp_prog prog);
......
137 137
       exported as a lusi *)
138 138
    raise (StopPhase1 prog);
139 139

  
140
 (* Optimization of prog: 
141
     - Unfold consts 
140
 (* Optimization of prog:
141
     - Unfold consts
142 142
     - eliminate trivial expressions
143 143
 *)
144 144
  (*
145
  let prog = 
145
  let prog =
146 146
    if !Options.const_unfold || !Options.optimization >= 5 then
147 147
      begin
148 148
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff