Project

General

Profile

Revision f9f06e7d

View differences:

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

  
58 58
  (* Importing source *)
59
  let _ = Modules.load_program ISet.empty prog in
59
  let _ = Modules.load ~is_header:false ISet.empty prog in
60 60

  
61 61
  (* Extracting dependencies (and updating Global.(type_env/clock_env) *)
62 62
  let dependencies = import_dependencies prog in
src/corelang.ml
175 175

  
176 176
let empty_contract =
177 177
  {
178
    consts = []; locals = []; assume = []; guarantees = []; modes = []; imports = []; spec_loc = Location.dummy_loc;
178
    consts = []; locals = []; stmts = []; assume = []; guarantees = []; modes = []; imports = []; spec_loc = Location.dummy_loc;
179 179
  }
180
    
180

  
181
(* For const declaration we do as for regular lustre node.
182
But for local flows we registered the variable and the lustre flow definition *)
181 183
let mk_contract_var id is_const type_opt expr loc =
182 184
  let typ = match type_opt with None -> mktyp loc Tydec_any | Some t -> t in
183
  let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None) in
184 185
  if is_const then
186
  let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, Some expr, None) in
185 187
  { empty_contract with consts = [v]; spec_loc = loc; }
186 188
  else
187
    { empty_contract with locals = [v]; spec_loc = loc; }
189
    let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, None, None) in
190
    let eq = mkeq loc ([id], expr) in 
191
    { empty_contract with locals = [v]; stmts = [Eq eq]; spec_loc = loc; }
188 192

  
189 193
let mk_contract_guarantees eexpr =
190 194
  { empty_contract with guarantees = [eexpr]; spec_loc = eexpr.eexpr_loc }
......
202 206
let merge_contracts ann1 ann2 = (* keeping the first item loc *)
203 207
  { consts = ann1.consts @ ann2.consts;
204 208
    locals = ann1.locals @ ann2.locals;
209
    stmts = ann1.stmts @ ann2.stmts;
205 210
    assume = ann1.assume @ ann2.assume;
206 211
    guarantees = ann1.guarantees @ ann2.guarantees;
207 212
    modes = ann1.modes @ ann2.modes;
src/error.ml
10 10
  | Unknown_library of ident
11 11
  | Wrong_number of ident
12 12
  | AlgebraicLoop
13
  | LoadError of string
13 14

  
14 15
let return_code kind =
15 16
  match kind with
......
21 22
  | Unknown_library _ -> 7
22 23
  | Wrong_number _ -> 8
23 24
  | AlgebraicLoop -> 9
24

  
25
  | LoadError _ -> 10
25 26

  
26 27
  let pp_error_msg fmt = function
27 28
  | Main_not_found ->
......
50 51
      "library %s.lusic has a different version number and may crash compiler.@.Please recompile the corresponding interface or source file.@."
51 52
      sym
52 53
  | AlgebraicLoop  -> assert false (* should have been handled yet *)
54
  | LoadError l -> 
55
    fprintf fmt
56
      "Load error: %s.@."
57
      l
53 58
     
54 59
let pp_warning loc pp_msg =
55 60
  Format.eprintf "%a@.Warning: %t@."
src/lustre_types.ml
131 131
type contract_import =
132 132
  { import_nodeid: ident; inputs: expr list; outputs: expr list; import_loc: Location.t }
133 133
    
134
type contract_desc = 
135
  {
136
(* TODO: 
137
   local variables 
138
   rename: assume/guarantee
139
           in behavior mode (id, requires/ensures)
140
   import contract
141
*)
142
       consts: var_decl list;
143
       locals: var_decl list;
144
       assume: eexpr list;
145
       guarantees: eexpr list;
146
       modes: contract_mode list;
147
       imports: contract_import list; 
148
       spec_loc: Location.t;
149
}
150 134

  
151 135

  
152 136
type offset =
......
178 162
   hand_annots: expr_annot list;
179 163
   hand_loc: Location.t}
180 164

  
165
type contract_desc = 
166
  {
167
    consts: var_decl list;
168
    locals: var_decl list;
169
    stmts: statement list;
170
    assume: eexpr list;
171
    guarantees: eexpr list;
172
    modes: contract_mode list;
173
    imports: contract_import list; 
174
    spec_loc: Location.t;
175
  }
176

  
181 177
type node_desc =
182 178
    {node_id: ident;
183 179
     mutable node_type: Types.type_expr;
src/main_lustre_compiler.ml
42 42
  begin
43 43
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
44 44
    let header = parse_header true (dirname ^ "/" ^ header_name) in
45
    ignore (Modules.load_header ISet.empty header);
45
    ignore (Modules.load ~is_header:true ISet.empty header);
46 46
    ignore (check_top_decls header); (* typing/clocking with an empty env *)
47 47
    create_dest_dir ();
48 48
    Log.report ~level:1
src/modules.ml
150 150
    raise exc
151 151
  )
152 152

  
153
let rec load_header_rec imported header =
154
  List.fold_left (fun imported decl ->
155
    match decl.top_decl_desc with
156
    | Node nd -> assert false
157
    | ImportedNode ind -> (add_imported_node ind.nodei_id decl; imported)
158
    | Const c -> (add_const true c.const_id decl; imported)
159
    | TypeDef tdef -> (add_type true tdef.tydef_id decl; imported)
160
    | Open (local, dep) ->
161
       let basename = Options_management.name_dependency (local, dep) in
162
       if ISet.mem basename imported then imported else
163
	 let lusic = import_dependency_aux decl.top_decl_loc (local, dep)
164
	 in load_header_rec (ISet.add basename imported) lusic.Lusic.contents
165
  ) imported header
166

  
167
let load_header imported header =
168
  try
169
    load_header_rec imported header
170
  with
171
    Corelang.Error (loc, err) as exc -> (
172
      Format.eprintf "Import error: %a%a@."
173
	Error.pp_error_msg err
174
	Location.pp_loc loc;
175
      raise exc
176
    );;
177 153

  
178
let rec load_program_rec imported program =
154
let rec load_rec ~is_header imported program =
179 155
  List.fold_left (fun imported decl ->
180 156
    match decl.top_decl_desc with
181
    | Node nd -> (add_node nd.node_id decl; imported)
182
    | ImportedNode ind -> assert false
183
    | Const c -> (add_const false c.const_id decl; imported)
184
    | TypeDef tdef -> (add_type false tdef.tydef_id decl; imported)
157
    | Node nd -> if is_header then
158
                   raise (Error(decl.top_decl_loc,
159
                                LoadError ("node " ^ nd.node_id ^ " declared in a header file")))  
160
                 else
161
                   (add_node nd.node_id decl; imported)
162
    | ImportedNode ind ->
163
       if is_header then
164
         (add_imported_node ind.nodei_id decl; imported)
165
       else
166
         raise (Error(decl.top_decl_loc,
167
                      LoadError ("imported node " ^ ind.nodei_id ^ " declared in a regular Lustre file")))  
168
    | Const c -> (add_const is_header c.const_id decl; imported)
169
    | TypeDef tdef -> (add_type is_header tdef.tydef_id decl; imported)
185 170
    | Open (local, dep) ->
186 171
       let basename = Options_management.name_dependency (local, dep) in
187 172
       if ISet.mem basename imported then imported else
188 173
	 let lusic = import_dependency_aux decl.top_decl_loc (local, dep)
189
	 in load_header_rec (ISet.add basename imported) lusic.Lusic.contents
174
	 in load_rec ~is_header:true (ISet.add basename imported) lusic.Lusic.contents
190 175
  ) imported program
191
    
192
let load_program imported program =
176

  
177
(* Iterates through lusi definitions and records them in the hashtbl. Open instructions are evaluated and update these hashtbl as well. node_table/type/table/consts_table *)
178
  
179
let load ~is_header imported program =
193 180
  try
194
    load_program_rec imported program
181
    load_rec ~is_header imported program
195 182
  with
196 183
    Corelang.Error (loc, err) as exc -> (
197 184
      Format.eprintf "Import error: %a%a@."
src/parsers/lexerLustreSpec.mll
25 25
  create_hashtable 20 [
26 26
  (* "true", TRUE; *)
27 27
  (* "false", FALSE; *)
28
  "function", FUNCTION;
28 29
  "if", IF;
29 30
  "then", THEN;
30 31
  "else", ELSE;
......
55 56
  "const", CONST;
56 57
  (* "include", INCLUDE; *)
57 58
  "assert", ASSERT;
58
  "ensure", ENSURE;
59
   "ensure", ENSURE;
59 60
  "require", REQUIRE;
60 61
  (* "observer", OBSERVER; *)
61 62
  "invariant", INVARIANT;
src/parsers/lexer_lustre.mll
61 61
  "contract", CONTRACT;
62 62
  "lib", LIB;
63 63
  "prototype", PROTOTYPE;
64
  "ensure", ENSURE;
65
  "require", REQUIRE;
66
  (* "observer", OBSERVER; *)
67
  "invariant", INVARIANT;
68
  "mode", MODE;
69
  "assume", ASSUME;
70
  "contract", CONTRACT;
71
  "guarantees", GUARANTEES;
72
  "exists", EXISTS;
73
  "forall", FORALL;
74
 
64 75
  "c_code", CCODE; (* not sure how it is used *)
65 76
  "matlab", MATLAB; (* same as above *)
66 77
]
src/parsers/parser_lustre.mly
202 202
				  nodei_prototype = $13;
203 203
				  nodei_in_lib = $14;})
204 204
     in
205
     (*add_imported_node $3 nd;*) [nd] } 
206
| CONTRACT node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract TEL 
207
    {let nd = mktop_decl true (ImportedNode
208
				 {nodei_id = $2;
209
				  nodei_type = Types.new_var ();
210
				  nodei_clock = Clocks.new_var true;
211
				  nodei_inputs = List.rev $4;
212
				  nodei_outputs = List.rev $9;
213
				  nodei_stateless = false (* By default we assume contracts as stateful *);
214
				  nodei_spec = Some $14;
215
				  nodei_prototype = None;
216
				  nodei_in_lib = [];})
217
     in
205 218
     (*add_imported_node $3 nd;*) [nd] }
206 219

  
207 220
prototype_opt:
......
350 363
	  mk_contract_mode $2 r e (get_loc())) $7 }	
351 364
| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract
352 365
    { merge_contracts (mk_contract_import $2  $4  $8 (get_loc())) $11 }
353
	
354 366

  
355 367
mode_content:
356 368
{ [], [] }

Also available in: Unified diff