Revision 3d1f9d9f
Added by LĂ©lio Brun over 2 years ago
src/spec_common.ml  

6  6  
7  7 
let is_false = function False > true  _ > false 
8  8  
9 
let type_of_l_value = function 

9 
let type_of_value = function 

10 
 Val v > v.Machine_code_types.value_type 

11 
 Tag (_, t) > t 

10  12 
 Var v > 
11  13 
v.var_type 
12  14 
 Memory ResetFlag > 
13  15 
Type_predef.type_bool 
14  16 
 Memory (StateVar v) > 
15  17 
v.var_type 
16 
 _ > assert false 

17  18  
18 
let expr_eq a b = 

19 
match a, b with


20 
 Var x, Var y >


21 
x = y


22 
 Memory r1, Memory r2 >


23 
r1 = r2


24 
 _ >


25 
false


19 
let expr_eq a b = a = b


20 
(* match a, b with *)


21 
(*  Var x, Var y > *)


22 
(* x = y *)


23 
(*  Memory r1, Memory r2 > *)


24 
(* r1 = r2 *)


25 
(*  _ > *)


26 
(* false *)


26  27  
27  28 
let rec red = function 
28  29 
 Equal (a, b) when expr_eq a b > 
...  ...  
124  125 
 hl > 
125  126 
let n = List.length hl in 
126  127 
And (List.mapi (fun k (t, spec) > 
127 
let c = if k = n  1 then GEqual (Var x, Tag t) else Equal (Var x, Tag t) in 

128 
let tag = Tag (t, x.var_type) in 

129 
let x = Var x in 

130 
let c = if k = n  1 then GEqual (x, tag) else Equal (x, tag) in 

128  131 
Imply (c, spec)) hl) 
129  132  
130  133 
let mk_assign_tr x v = Equal (Var x, Val v) 
Also available in: Unified diff
more agressive optim propagation in spec in order to remove unecessarry existential variables that were eliminated (helps the solvers)