Project

General

Profile

« Previous | Next » 

Revision 782742b6

Added by Pierre-Loïc Garoche about 5 years ago

Merged unstable with seahorn

View differences:

src/normalization.ml
13 13
open LustreSpec
14 14
open Corelang
15 15
open Format
16

  
17
let expr_true loc ck =
18
{ expr_tag = Utils.new_tag ();
19
  expr_desc = Expr_const (Const_tag tag_true);
20
  expr_type = Type_predef.type_bool;
21
  expr_clock = ck;
22
  expr_delay = Delay.new_var ();
23
  expr_annot = None;
24
  expr_loc = loc }
25

  
26
let expr_false loc ck =
27
{ expr_tag = Utils.new_tag ();
28
  expr_desc = Expr_const (Const_tag tag_false);
29
  expr_type = Type_predef.type_bool;
30
  expr_clock = ck;
31
  expr_delay = Delay.new_var ();
32
  expr_annot = None;
33
  expr_loc = loc }
34

  
35
let expr_once loc ck =
36
 { expr_tag = Utils.new_tag ();
37
  expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck);
38
  expr_type = Type_predef.type_bool;
39
  expr_clock = ck;
40
  expr_delay = Delay.new_var ();
41
  expr_annot = None;
42
  expr_loc = loc }
43

  
44
let is_expr_once =
45
  let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in
46
  fun expr -> Corelang.is_eq_expr expr dummy_expr_once
47

  
48
let unfold_arrow expr =
49
 match expr.expr_desc with
50
 | Expr_arrow (e1, e2) ->
51
    let loc = expr.expr_loc in
52
    let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
53
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
54
 | _                   -> assert false
55

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

  
59
(* Generate a new local [node] variable *)
60
let mk_fresh_var node loc ty ck =
61
  let vars = get_node_vars node in
62
  let rec aux () =
63
  incr cpt_fresh;
64
  let s = Printf.sprintf "__%s_%d" node.node_id !cpt_fresh in
65
  if List.exists (fun v -> v.var_id = s) vars then aux () else
66
  {
67
    var_id = s;
68
    var_orig = false;
69
    var_dec_type = dummy_type_dec;
70
    var_dec_clock = dummy_clock_dec;
71
    var_dec_const = false;
72
    var_dec_value = None;
73
    var_type = ty;
74
    var_clock = ck;
75
    var_loc = loc
76
  }
77
  in aux ()
78

  
79
(* Get the equation in [defs] with [expr] as rhs, if any *)
80
let get_expr_alias defs expr =
81
 try Some (List.find (fun eq -> is_eq_expr eq.eq_rhs expr) defs)
82
 with
83
 | Not_found -> None
84
  
85
(* Replace [expr] with (tuple of) [locals] *)
86
let replace_expr locals expr =
87
 match locals with
88
 | []  -> assert false
89
 | [v] -> { expr with
90
   expr_tag = Utils.new_tag ();
91
   expr_desc = Expr_ident v.var_id }
92
 | _   -> { expr with
93
   expr_tag = Utils.new_tag ();
94
   expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
95

  
96
let unfold_offsets e offsets =
97
  let add_offset e d =
98
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
99
    let res = *)
100
    { e with
101
      expr_tag = Utils.new_tag ();
102
      expr_loc = d.Dimension.dim_loc;
103
      expr_type = Types.array_element_type e.expr_type;
104
      expr_desc = Expr_access (e, d) }
105
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
106
  in
107
 List.fold_left add_offset e offsets
108

  
109
(* Create an alias for [expr], if none exists yet *)
110
let mk_expr_alias node (defs, vars) expr =
111
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
112
  match get_expr_alias defs expr with
113
  | Some eq ->
114
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
115
    (defs, vars), replace_expr aliases expr
116
  | None    ->
117
    let new_aliases =
118
      List.map2
119
	(mk_fresh_var node expr.expr_loc)
120
	(Types.type_list_of_type expr.expr_type)
121
	(Clocks.clock_list_of_clock expr.expr_clock) in
122
    let new_def =
123
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
124
    in
125
    (* Format.eprintf "Checking def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
126
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
127

  
128
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
129
   and [opt] is true *)
130
let mk_expr_alias_opt opt node (defs, vars) expr =
131
(*Format.eprintf "mk_expr_alias_opt %B %a %a %a@." opt Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
132
  match expr.expr_desc with
133
  | Expr_ident alias ->
134
    (defs, vars), expr
135
  | _                ->
136
    match get_expr_alias defs expr with
137
    | Some eq ->
138
      let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
139
      (defs, vars), replace_expr aliases expr
140
    | None    ->
141
      if opt
142
      then
143
	let new_aliases =
144
	  List.map2
145
	    (mk_fresh_var node expr.expr_loc)
146
	    (Types.type_list_of_type expr.expr_type)
147
	    (Clocks.clock_list_of_clock expr.expr_clock) in
148
	let new_def =
149
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
150
	in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
151
      else
152
	(defs, vars), expr
16
open Normalization_common
153 17

  
154 18
(* Create a (normalized) expression from [ref_e],
155 19
   replacing description with [norm_d],

Also available in: Unified diff