Project

General

Profile

Revision 8f1c7e91

View differences:

src/clock_calculus.ml
251 251
          cr1.carrier_desc <- Carry_link cr2;
252 252
          update_scope_carrier cr1.carrier_scoped cr2
253 253
        end
254
    | _,_ -> (assert false)
254
    | _,_ -> assert false
255

  
256
(* Semi-unifies two clock carriers *)
257
let semi_unify_carrier cr1 cr2 =
258
  let cr1 = carrier_repr cr1 in
259
  let cr2 = carrier_repr cr2 in
260
  if cr1=cr2 then ()
261
  else
262
    match cr1.carrier_desc, cr2.carrier_desc with
263
    | Carry_const id1, Carry_const id2 ->
264
      if id1 <> id2 then raise (Mismatch (cr1, cr2))
265
    | Carry_const _, Carry_name ->
266
      begin
267
	cr2.carrier_desc <- Carry_link cr1;
268
	update_scope_carrier cr2.carrier_scoped cr1
269
      end
270
    | Carry_name, Carry_const _ -> raise (Mismatch (cr1, cr2))
271
    | Carry_name, Carry_name ->
272
      if cr1.carrier_id < cr2.carrier_id then
273
        begin
274
          cr2.carrier_desc <- Carry_link cr1;
275
          update_scope_carrier cr2.carrier_scoped cr1
276
        end
277
      else
278
        begin
279
          cr1.carrier_desc <- Carry_link cr2;
280
          update_scope_carrier cr1.carrier_scoped cr2
281
        end
282
    | _,_ -> assert false
255 283

  
256 284
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify
257 285
    (ck1,ck2)] if the clocks are not unifiable.*)
......
355 383
          subsume ck2 (CSet_pck (b,(a,b)));
356 384
          let ck2' = simplify (new_ck (Pck_phase (ck2,(-a,b))) true) in
357 385
          unify pck1' ck2'
358
      (* Corner case for some functions like ite, need to unify guard clock
359
	 with output clocks *)
360
(*
361
      | Ctuple ckl, (Cvar _) -> List.iter (unify ck2) ckl
362
      | (Cvar _), Ctuple ckl ->	List.iter (unify ck1) ckl
363
*)
386
      | Cunivar _, _ | _, Cunivar _ -> ()
387
      | _,_ -> raise (Unify (ck1,ck2))
388

  
389
(** [unify ck1 ck2] semi-unifies clocks [ck1] and [ck2]. Raises [Unify
390
    (ck1,ck2)] if the clocks are not semi-unifiable.*)
391
let rec semi_unify ck1 ck2 =
392
  let ck1 = repr ck1 in
393
  let ck2 = repr ck2 in
394
  if ck1=ck2 then
395
    ()
396
  else
397
      match ck1.cdesc,ck2.cdesc with
398
      | Cvar cset1,Cvar cset2->
399
          if ck1.cid < ck2.cid then
400
            begin
401
              ck2.cdesc <- Clink (simplify ck1);
402
              update_scope ck2.cscoped ck1
403
            end
404
          else
405
            begin
406
              ck1.cdesc <- Clink (simplify ck2);
407
              update_scope ck1.cscoped ck2
408
            end
409
      | (Cvar cset,_) -> raise (Unify (ck1,ck2))
410
      | (_, (Cvar cset)) when (not (occurs ck2 ck1)) ->
411
          update_scope ck2.cscoped ck1;
412
          ck2.cdesc <- Clink (simplify ck1)
413
      | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
414
          semi_unify_carrier cr1 cr2;
415
          semi_unify ck1' ck2'
416
      | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
417
          raise (Unify (ck1,ck2))
418
      | Carrow (c1,c2), Carrow (c1',c2') ->
419
	begin
420
          semi_unify c1 c1';
421
	  semi_unify c2 c2'
422
	end
423
      | Ctuple ckl1, Ctuple ckl2 ->
424
          if (List.length ckl1) <> (List.length ckl2) then
425
            raise (Unify (ck1,ck2));
426
          List.iter2 semi_unify ckl1 ckl2
427
      | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
428
          semi_unify_carrier c1 c2;
429
          semi_unify ck' ck''
364 430
      | Cunivar _, _ | _, Cunivar _ -> ()
365 431
      | _,_ -> raise (Unify (ck1,ck2))
366 432

  
......
442 508
  | Mismatch (cr1,cr2) ->
443 509
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
444 510

  
511
let try_semi_unify ck1 ck2 loc =
512
  try
513
    semi_unify ck1 ck2
514
  with
515
  | Unify (ck1',ck2') ->
516
    raise (Error (loc, Clock_clash (ck1',ck2')))
517
  | Subsume (ck,cset) ->
518
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
519
  | Mismatch (cr1,cr2) ->
520
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
521

  
445 522
(* Checks whether ck1 is a subtype of ck2 *)
446 523
let rec clock_subtyping ck1 ck2 =
447 524
  match (repr ck1).cdesc, (repr ck2).cdesc with
......
775 852
let clock_prog env decls =
776 853
  List.fold_left (fun e decl -> clock_top_decl e decl) env decls
777 854

  
855
(* Once the Lustre program is fully clocked,
856
   we must get back to the original description of clocks,
857
   with constant parameters, instead of unifiable internal variables. *)
858

  
859
(* The following functions aims at 'unevaluating' carriers occuring in clock expressions,
860
   i.e. replacing unifiable second_order variables with the original carrier names.
861
   Once restored in this formulation, clocks may be meaningfully printed.
862
*)
863
let uneval_vdecl_generics vdecl =
864
 if Types.is_clock_type vdecl.var_type
865
 then
866
   match get_carrier_name vdecl.var_clock with
867
   | None    -> (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false)
868
   | Some cr -> Clocks.uneval vdecl.var_id cr
869

  
870
let uneval_node_generics vdecls =
871
  List.iter uneval_vdecl_generics vdecls
872

  
873
let uneval_top_generics decl =
874
  match decl.top_decl_desc with
875
  | Node nd ->
876
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
877
  | ImportedNode nd ->
878
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
879
  | ImportedFun nd ->
880
      ()
881
  | Consts clist -> ()
882
  | Open _  -> ()
883

  
884
let uneval_prog_generics prog =
885
 List.iter uneval_top_generics prog
886

  
778 887
let check_env_compat header declared computed =
888
  uneval_prog_generics header;
779 889
  Env.iter declared (fun k decl_clock_k -> 
780 890
    let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
781
    try_unify decl_clock_k computed_c Location.dummy_loc
891
    try_semi_unify decl_clock_k computed_c Location.dummy_loc
782 892
  ) 
783 893
(* Local Variables: *)
784 894
(* compile-command:"make -C .." *)
src/clocks.ml
121 121
       needs to be considered here *)
122 122
  | _ -> failwith "Internal error: not an arrow clock"
123 123

  
124
let get_carrier_name ck =
125
 match (repr ck).cdesc with
126
 | Ccarrying (cr, _) -> Some cr
127
 | _                 -> None
128

  
124 129
let uncarrier ck =
125 130
 match ck.cdesc with
126
 | Ccarrying (cr, ck') -> ck'
127
 | _                   -> ck
131
 | Ccarrying (_, ck') -> ck'
132
 | _                  -> ck
128 133

  
129 134
(* Removes all links in a clock. Only used for clocks
130 135
   simplification though. *)
......
268 273
let rec print_carrier fmt cr =
269 274
 (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
270 275
  match cr.carrier_desc with
271
  | Carry_const id -> fprintf fmt "'%s'" id
276
  | Carry_const id -> fprintf fmt "%s" id
272 277
  | Carry_name ->
273
      fprintf fmt "?%s" (name_of_carrier cr.carrier_id)
278
      fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
274 279
  | Carry_var ->
275
    fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
280
    fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
276 281
  | Carry_link cr' ->
277 282
    print_carrier fmt cr'
278 283

  
......
512 517
    fprintf fmt " (where %a)"
513 518
      (fprintf_list ~sep:", " print_cvar) cvars
514 519

  
520
(* prints only the Con components of a clock, useful for printing nodes *)
521
let rec print_ck_suffix fmt ck =
522
  let ck = simplify ck in
523
  match ck.cdesc with
524
  | Carrow _
525
  | Ctuple _
526
  | Cvar _
527
  | Cunivar _   -> ()
528
  | Con (ck,c,l) ->
529
    fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
530
  | Clink ck' ->
531
    print_ck_suffix fmt ck'
532
  | Ccarrying (cr,ck') ->
533
    fprintf fmt "%a" print_ck_suffix ck'
534
  | _ -> assert false
535

  
515 536
let pp_error fmt = function
516 537
  | Clock_clash (ck1,ck2) ->
517 538
      reset_names ();
......
552 573
      print_ck ck_node
553 574
      print_ck ck
554 575

  
576
let uneval const cr =
577
 (*Format.printf "uneval %s %a@." const print_carrier cr;*)
578
  let cr = carrier_repr cr in
579
  match cr.carrier_desc with
580
  | Carry_var -> cr.carrier_desc <- Carry_const const
581
  | _         -> assert false
555 582

  
556 583
(* Local Variables: *)
557 584
(* compile-command:"make -C .." *)
src/dimension.ml
347 347
  | Dident id1, Dident id2 when id1 = id2 -> ()
348 348
  | _ -> raise (Unify (dim1, dim2))
349 349

  
350
(* unification with the constraint that dim1 is an instance of dim2 *)
350 351
let rec semi_unify dim1 dim2 =
351 352
  let dim1 = repr dim1 in
352 353
  let dim2 = repr dim2 in
src/main_lustre_compiler.ml
28 28

  
29 29
let usage = "Usage: lustrec [options] <source-file>"
30 30

  
31
let extensions = [".ec";".lus"]
31
let extensions = [".ec"; ".lus"; ".lusi"]
32 32

  
33 33
let type_decls env decls =  
34 34
  report ~level:1 (fun fmt -> fprintf fmt ".. typing@,@?");
......
79 79

  
80 80
let check_lusi header =
81 81
  let new_tenv = type_decls Basic_library.type_env header in   (* Typing *)
82
  let new_cenv: Clocks.clock_expr Utils.IMap.t = clock_decls Basic_library.clock_env header in   (* Clock calculus *)
82
  let new_cenv = clock_decls Basic_library.clock_env header in   (* Clock calculus *)
83 83
  header, new_tenv, new_cenv
84 84
    
85 85
let rec compile basename extension =
......
192 192
      let lusi_out = open_out lusi_name in
193 193
      let lusi_fmt = formatter_of_out_channel lusi_out in
194 194
      Typing.uneval_prog_generics prog;
195
      Clock_calculus.uneval_prog_generics prog;
195 196
      Printers.pp_lusi_header lusi_fmt source_name prog
196 197
    )
197 198
    | (Types.Error (loc,err)) as exc ->
198 199
      Format.eprintf "Type mismatch between computed type and declared type in lustre interface file: %a@]@."
199 200
	Types.pp_error err;
200 201
      raise exc
202
    | Clocks.Error (loc, err) as exc ->
203
      Format.eprintf "Clock mismatch between computed clock and declared clock in lustre interface file: %a@]@."
204
	Clocks.pp_error err;
205
      raise exc
201 206
  in
202 207

  
203 208
  (* Computes and stores generic calls for each node,
......
226 231

  
227 232
  (* Printing code *)
228 233
  let basename    =  Filename.basename basename in
234
  let destname = !Options.dest_dir ^ "/" ^ basename in
229 235
  let _ = match !Options.output with
230 236
      "C" -> 
231 237
	begin
232
	  let destname = !Options.dest_dir ^ "/" ^ basename in
233 238
	  let header_file = destname ^ ".h" in (* Could be changed *)
234 239
	  let source_file = destname ^ ".c" in (* Could be changed *)
235 240
	  let makefile_file = destname ^ ".makefile" in (* Could be changed *)
......
268 273
      end
269 274
    | "horn" ->
270 275
      begin
271
	let destname = !Options.dest_dir ^ "/" ^ basename in
272 276
	let source_file = destname ^ ".smt2" in (* Could be changed *)
273 277
	let source_out = open_out source_file in
274 278
	let fmt = formatter_of_out_channel source_out in
......
286 290
    let basename = Filename.chop_suffix filename ext in
287 291
    compile basename ext
288 292
  else
289
    raise (Arg.Bad ("Can only compile *.lus or *.ec files"))
293
    raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
290 294

  
291 295
let _ =
292 296
  Corelang.add_internal_funs ();
src/printers.ml
50 50

  
51 51
and pp_var fmt id = fprintf fmt "%s%s: %a" (if id.var_dec_const then "const " else "") id.var_id Types.print_ty id.var_type
52 52

  
53
and pp_node_var fmt id = fprintf fmt "%s%s: %a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type
53
and pp_node_var fmt id = fprintf fmt "%s%s: %a%a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type Clocks.print_ck_suffix id.var_clock
54 54

  
55 55
and pp_expr fmt expr =
56 56
  match expr.expr_desc with
src/types.ml
176 176
 | Tstatic (d, _) -> Some d
177 177
 | _              -> None
178 178

  
179
let is_clock_type ty =
180
 match (repr ty).tdesc with
181
 | Tclock _ -> true
182
 | _        -> false
183

  
179 184
let rec is_dimension_type ty =
180 185
 match (repr ty).tdesc with
181 186
 | Tint
src/typing.ml
678 678
   i.e. replacing unifiable second_order variables with the original static parameters.
679 679
   Once restored in this formulation, dimensions may be meaningfully printed.
680 680
*)
681
(*
682
let uneval_vdecl_generics vdecl ty =
683
 if vdecl.var_dec_const
684
 then
685
   match get_static_value ty with
686
   | None   -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
687
   | Some d -> Dimension.unify d (Dimension.mkdim_ident vdecl.var_loc vdecl.var_id)
688

  
689
let uneval_node_generics vdecls =
690
  let inst_typ_vars = ref [] in
691
  let inst_dim_vars = ref [] in
692
  let inst_ty_list = List.map (fun v -> instantiate inst_typ_vars inst_dim_vars v.var_type) vdecls in
693
  List.iter2 (fun v ty -> uneval_vdecl_generics v ty) vdecls inst_ty_list;
694
  List.iter2 (fun v ty -> generalize ty; v.var_type <- ty) vdecls inst_ty_list
695
*)
696 681
let uneval_vdecl_generics vdecl =
697 682
 if vdecl.var_dec_const
698 683
 then
......
717 702
let uneval_prog_generics prog =
718 703
 List.iter uneval_top_generics prog
719 704

  
720
let check_env_compat header declared computed =
721
  (try 
722
     uneval_prog_generics header
723
   with e -> raise e);
705
let check_env_compat header declared computed = 
706
  uneval_prog_generics header;
724 707
  Env.iter declared (fun k decl_type_k -> 
725 708
    let computed_t = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
726 709
    (*Types.print_ty Format.std_formatter decl_type_k;
test/src/arrays_arnaud/dummy_lib.lusi
1
node test(x:int) returns (t:int^2);
2

  
3
function _MatMul_real (
4
	const n, m, p : int ;
5
	in1 : real^n^m ;
6
	in2 : real^m^p)
7
returns (
8
	out : real^n^p) ;
9

  
10
function _Vect_Leqt_real (
11
	const n : int ;
12
	in : real^n ;
13
	in2 : real^n)
14
returns (
15
	out : bool^n) ;
16

  
17
node imp1(const m:int; a:int^(3*m)) returns (c:int^m);
18

  
19
node imp2(const n:int; a:int^n) returns (d:int^n);
test/src/clocks/oversampling0.lus
18 18
var toto:int;
19 19
let
20 20
  toto = 1 ;
21
  c = true fby false fby c;
21
  c = toto = 0 (*true fby false fby c*);
22 22
  out = g(x,toto=0);
23 23
tel
24 24
*)
test/test-compile.sh
51 51
        fi
52 52
    fi
53 53
    popd > /dev/null
54
    echo "lustrec ($rlustrec1), gcc($rgcc1), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
54
    echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
55 55
    done < $file_list
56 56
}
57 57

  
......
78 78
    else
79 79
        rgcc2="VALID"
80 80
    fi	
81
    echo "lustrec inlined ($rlustrec2), gcc ($rgcc2),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
81
    echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
82 82
    popd > /dev/null
83 83
done < $file_list
84 84
}
......
106 106
    fi	
107 107
	# Cheching witness
108 108
    pushd $build > /dev/null
109
    lustrec -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 2>/dev/null
109
    $LUSTREC -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 2>/dev/null
110 110
    popd > /dev/null
111 111
    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
112 112
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
......
119 119
	rinlining="INVALID"
120 120
	exit 1
121 121
    fi  
122
    echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
122
    echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
123 123
    popd > /dev/null
124 124
done < $file_list
125 125

  
......
146 146
    else
147 147
        rhorn="VALID"
148 148
    fi
149
    echo "horn-pdr ($rhorn), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
149
    echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
150 150
    popd > /dev/null
151 151
done < $file_list
152 152
}

Also available in: Unified diff