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/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