Project

General

Profile

« Previous | Next » 

Revision 9c4624e4

Added by Teme Kahsai about 9 years ago

do not use lusi for horn, and some logging for horn

View differences:

src/backends/Horn/horn_backend.ml
328 328
       Format.pp_print_newline fmt ();
329 329

  
330 330
       (* Rule for init *)
331
       (* Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." *)
332
       (*   (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs *)
333
       (*   pp_machine_init_name m.mname.node_id *)
334
       (*   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); *)
335

  
336
       (* (\* Rule for step *\) *)
337
       (* Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." *)
338
       (*   (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs *)
339
       (*   pp_machine_step_name m.mname.node_id *)
340
       (*   (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); *)
341

  
331
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
332
	 (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
333
	 pp_machine_init_name m.mname.node_id
334
	 (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
342 335

  
343 336
      (* Adding assertions *)
344 337
       (match m.mstep.step_asserts with
......
373 366
                           (pp_conj pp_val) assertsl
374 367
                           pp_machine_step_name m.mname.node_id
375 368
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
376
	    (* Format.fprintf fmt " @[<v 2>%a@]@ @.@.@." *)
377
            (*                 (pp_conj pp_val) assertsl; *)
378

  
379 369
          end
380 370
       );
381

  
382

  
383 371
     end
384 372
    end
385 373

  
......
445 433
    (pp_conj pp_var) main_output
446 434
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
447 435
    ;
448
   Format.fprintf fmt "(query ERR)@."
436
   if !Options.horn_query then Format.fprintf fmt "(query ERR)@."
449 437

  
450 438

  
451 439
let cex_computation machines fmt node machine =
......
534 522

  
535 523

  
536 524
let translate fmt basename prog machines =
525
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification");
537 526
  List.iter (print_machine machines fmt) (List.rev machines);
538 527
  main_print machines fmt
539 528

  
540 529

  
541 530
let traces_file fmt basename prog machines =
542
  (* Format.fprintf fmt *)
543
  (*   "; Horn code traceability generated by %s@.; SVN version number %s@.@." *)
544
  (*   (Filename.basename Sys.executable_name) *)
545
  (*   Version.number; *)
546 531

  
547 532
  Format.fprintf fmt
548 533
  "<?xml version=\"1.0\"?>\n<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">\n";
......
622 607
	memories_old
623 608
    in
624 609

  
625
    let pp_prefix_rev fmt prefix =
626
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
627
    in
610
    (* let pp_prefix_rev fmt prefix = *)
611
    (*   Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix) *)
612
    (* in *)
628 613

  
629
  let pp_prefix_rev fmt prefix =
614
    let pp_prefix_rev fmt prefix =
630 615
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
631 616
    in
632 617

  
......
663 648
  ) (List.rev machines);
664 649
  Format.fprintf fmt "</Traces>@.";
665 650

  
651
          (* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *)
652
   (* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" *)
653
   (*                                  pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old); *)
654

  
666 655
(* Local Variables: *)
667 656
(* compile-command:"make -C ../.." *)
668 657
(* End: *)
src/main_lustre_compiler.ml
149 149
    raise exc
150 150
    end;
151 151
  *)
152
  
152

  
153 153
  (* Creating destination directory if needed *)
154 154
  create_dest_dir ();
155 155

  
156 156
  (* Compatibility with Lusi *)
157 157
  (* Checking the existence of a lusi (Lustre Interface file) *)
158
  let extension = ".lusi" in
159
  compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
158
  match !Options.output with
159
    "C" ->
160
      begin
161
        let extension = ".lusi" in
162
        compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
163
      end
164
   |_ -> ();
160 165

  
161 166
  Typing.uneval_prog_generics prog;
162 167
  Clock_calculus.uneval_prog_generics prog;
......
170 175
      let _ = Clock_calculus.clock_prog clock_env orig in
171 176
      Typing.uneval_prog_generics orig;
172 177
      Clock_calculus.uneval_prog_generics orig;
173
      Inliner.witness 
178
      Inliner.witness
174 179
	basename
175 180
	!Options.main_node
176 181
	orig prog type_env clock_env
......
234 239
      machine_code
235 240
  in
236 241

  
237
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
242
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
238 243
  (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
239 244
  machine_code);
240 245

  
......
259 264
      machine_code
260 265
  in
261 266

  
267

  
262 268
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
263 269
  (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
264 270
  machine_code);
......
289 295
      Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
290 296
      end
291 297
    | "horn" ->
292
      begin
298
       begin
293 299
	let source_file = destname ^ ".smt2" in (* Could be changed *)
294 300
	let source_out = open_out source_file in
295 301
	let fmt = formatter_of_out_channel source_out in
src/normalization.ml
53 53
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
54 54
 | _                   -> assert false
55 55

  
56
let unfold_arrow_active = ref true 
56
let unfold_arrow_active = ref true
57 57
let cpt_fresh = ref 0
58 58

  
59 59
(* Generate a new local [node] variable *)
......
131 131
  match expr.expr_desc with
132 132
  | Expr_ident alias ->
133 133
    defvars, expr
134
  | _                -> 
134
  | _                ->
135 135
    if opt
136 136
    then
137 137
      mk_expr_alias node defvars expr
138 138
    else
139 139
      defvars, expr
140 140

  
141
(* Create a (normalized) expression from [ref_e], 
141
(* Create a (normalized) expression from [ref_e],
142 142
   replacing description with [norm_d],
143
   taking propagated [offsets] into account 
143
   taking propagated [offsets] into account
144 144
   in order to change expression type *)
145 145
let mk_norm_expr offsets ref_e norm_d =
146 146
(*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
......
161 161
let rec normalize_expr ?(alias=true) node offsets defvars expr =
162 162
(*  Format.eprintf "normalize %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
163 163
  match expr.expr_desc with
164
  | Expr_const _ 
164
  | Expr_const _
165 165
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
166 166
  | Expr_array elist ->
167 167
    let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
......
175 175
    normalize_expr ~alias:alias node (List.tl offsets) defvars e1
176 176
  | Expr_access (e1, d) ->
177 177
    normalize_expr ~alias:alias node (d::offsets) defvars e1
178
  | Expr_tuple elist -> 
178
  | Expr_tuple elist ->
179 179
    let defvars, norm_elist =
180 180
      normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias) defvars elist in
181 181
    defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
182
  | Expr_appl (id, args, None) 
183
      when Basic_library.is_internal_fun id 
182
  | Expr_appl (id, args, None)
183
      when Basic_library.is_internal_fun id
184 184
	&& Types.is_array_type expr.expr_type ->
185
    let defvars, norm_args = 
186
      normalize_list 
185
    let defvars, norm_args =
186
      normalize_list
187 187
	alias
188 188
	node
189
	offsets 
190
	(fun _ -> normalize_array_expr ~alias:true) 
191
	defvars 
192
	(expr_list_of_expr args) 
189
	offsets
190
	(fun _ -> normalize_array_expr ~alias:true)
191
	defvars
192
	(expr_list_of_expr args)
193 193
    in
194 194
    defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
195 195
  | Expr_appl (id, args, None) when Basic_library.is_internal_fun id ->
......
233 233
    let defvars, norm_hl = normalize_branches node offsets defvars hl in
234 234
    let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
235 235
    mk_expr_alias_opt alias node defvars norm_expr
236
  
236

  
237 237
(* Creates a conditional with a merge construct, which is more lazy *)
238 238
(*
239 239
let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
......
309 309
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
310 310
  defvars', {eq with eq_lhs = lhs' }
311 311

  
312
let rec normalize_eq node defvars eq = 
312
let rec normalize_eq node defvars eq =
313 313
  match eq.eq_rhs.expr_desc with
314 314
  | Expr_pre _
315 315
  | Expr_fby _  ->
......
334 334
    let norm_eq = { eq with eq_rhs = norm_rhs } in
335 335
    norm_eq::defs', vars'
336 336

  
337
(** normalize_node node returns a normalized node, 
338
    ie. 
337
(** normalize_node node returns a normalized node,
338
    ie.
339 339
    - updated locals
340 340
    - new equations
341
    - 
341
    -
342 342
*)
343
let normalize_node node = 
343
let normalize_node node =
344 344
  cpt_fresh := 0;
345 345
  let inputs_outputs = node.node_inputs@node.node_outputs in
346 346
  let is_local v =
347 347
    List.for_all ((!=) v) inputs_outputs in
348 348
  let orig_vars = inputs_outputs@node.node_locals in
349
  let defs, vars = 
349
  let defs, vars =
350 350
    List.fold_left (normalize_eq node) ([], orig_vars) (get_node_eqs node) in
351 351
  (* Normalize the asserts *)
352
  let vars, assert_defs, asserts = 
352
  let vars, assert_defs, asserts =
353 353
    List.fold_left (
354 354
    fun (vars, def_accu, assert_accu) assert_ ->
355 355
      let assert_expr = assert_.assert_expr in
356
      let (defs, vars'), expr = 
357
	normalize_expr 
358
	  ~alias:true 
359
	  node 
356
      let (defs, vars'), expr =
357
	normalize_expr
358
	  ~alias:true
359
	  node
360 360
	  [] (* empty offset for arrays *)
361 361
	  ([], vars) (* defvar only contains vars *)
362 362
	  assert_expr
363 363
      in
364
      (* Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars'; *)
364
      (*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
365 365
      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
366 366
    ) (vars, [], []) node.node_asserts in
367 367
  let new_locals = List.filter is_local vars in
368
  (* Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals; *)
368
  (*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
369 369

  
370 370
  let new_annots =
371 371
    if !Options.traces then
372 372
      begin
373
	(* Compute traceability info: 
373
	(* Compute traceability info:
374 374
	   - gather newly bound variables
375
	   - compute the associated expression without aliases     
375
	   - compute the associated expression without aliases
376 376
	*)
377 377
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
378 378
	let norm_traceability = {
379 379
	  annots = List.map (fun v ->
380 380
	    let eq =
381 381
	      try
382
		List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs 
382
		List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs
383 383
	      with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
384 384
	    let expr = substitute_expr diff_vars defs eq.eq_rhs in
385 385
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
386 386
	    (["traceability"], pair)
387 387
	  ) diff_vars;
388 388
	  annot_loc = Location.dummy_loc
389
	} 
389
	}
390 390
	in
391 391
	norm_traceability::node.node_annot
392 392
      end
......
395 395
  in
396 396

  
397 397
  let node =
398
  { node with 
399
    node_locals = new_locals; 
398
  { node with
399
    node_locals = new_locals;
400 400
    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
401 401
    node_asserts = asserts;
402 402
    node_annot = new_annots;
403 403
  }
404
  in ((*Printers.pp_node Format.err_formatter node;*) 
404
  in ((*Printers.pp_node Format.err_formatter node;*)
405 405
    node
406 406
)
407 407

  
......
413 413
    Hashtbl.replace Corelang.node_table nd.node_id decl';
414 414
    decl'
415 415
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
416
  
417
let normalize_prog decls = 
416

  
417
let normalize_prog decls =
418 418
  List.map normalize_decl decls
419 419

  
420 420
(* Local Variables: *)

Also available in: Unified diff