Project

General

Profile

« Previous | Next » 

Revision 36454535

Added by Pierre-Loïc Garoche over 10 years ago

Merged horn_traces branch

View differences:

src/normalization.ml
196 196
    let defvars, norm_elist =
197 197
      normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias) defvars elist in
198 198
    defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
199
  | Expr_appl (id, args, None) when Basic_library.is_internal_fun id && Types.is_array_type expr.expr_type ->
200
    let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
199
  | Expr_appl (id, args, None) 
200
      when Basic_library.is_internal_fun id 
201
	&& Types.is_array_type expr.expr_type ->
202
    let defvars, norm_args = 
203
      normalize_list 
204
	alias
205
	node
206
	offsets 
207
	(fun _ -> normalize_array_expr ~alias:true) 
208
	defvars 
209
	(expr_list_of_expr args) 
210
    in
201 211
    defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
202 212
  | Expr_appl (id, args, None) when Basic_library.is_internal_fun id ->
203 213
    let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in
......
341 351
    let norm_eq = { eq with eq_rhs = norm_rhs } in
342 352
    norm_eq::defs', vars'
343 353

  
354
(** normalize_node node returns a normalized node, 
355
    ie. 
356
    - updated locals
357
    - new equations
358
    - 
359
*)
344 360
let normalize_node node = 
345 361
  cpt_fresh := 0;
346 362
  let inputs_outputs = node.node_inputs@node.node_outputs in
347 363
  let is_local v =
348 364
    List.for_all ((!=) v) inputs_outputs in
365
  let orig_vars = inputs_outputs@node.node_locals in
349 366
  let defs, vars = 
350
    List.fold_left (normalize_eq node) ([], inputs_outputs@node.node_locals) node.node_eqs in
367
    List.fold_left (normalize_eq node) ([], orig_vars) node.node_eqs in
368
  (* Normalize the asserts *)
369
  let vars, assert_defs, asserts = 
370
    List.fold_left (
371
    fun (vars, def_accu, assert_accu) assert_ ->
372
      let assert_expr = assert_.assert_expr in
373
      let (defs, vars'), expr = 
374
	normalize_expr 
375
	  ~alias:false 
376
	  node 
377
	  [] (* empty offset for arrays *)
378
	  ([], vars) (* defvar only contains vars *)
379
	  assert_expr
380
      in
381
      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
382
    ) (vars, [], []) node.node_asserts in
351 383
  let new_locals = List.filter is_local vars in
384
  (* Compute tracebaility info: 
385
     - gather newly bound variables
386
     - compute the associated expression without aliases     
387
  *)
388
  let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
389
  let norm_traceability = {
390
    annots = 
391
      List.map 
392
	(fun v -> 
393
	  let expr = substitute_expr diff_vars defs (
394
	    let eq = List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs in
395
	    eq.eq_rhs) in 
396
	  let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
397
	  ["horn_backend";"trace"], pair 
398
    ) 
399
    diff_vars ;
400
    annot_loc = Location.dummy_loc
401
  }
402

  
403
  in
352 404
  let node =
353
  { node with node_locals = new_locals; node_eqs = defs }
405
  { node with 
406
    node_locals = new_locals; 
407
    node_eqs = defs @ assert_defs;
408
    node_asserts = asserts;
409
    node_annot = norm_traceability::node.node_annot;
410
  }
354 411
  in ((*Printers.pp_node Format.err_formatter node;*) node)
355 412

  
356 413
let normalize_decl decl =

Also available in: Unified diff