Project

General

Profile

Revision 9a9058f4

View differences:

src/corelang.ml
516 516
 List.sort (fun (t, _) (t', _) -> compare t t') hl
517 517

  
518 518
let num_10 = Num.num_of_int 10
519
  
519

  
520
let cst_real_to_num n i =
521
  Num.(n // (num_10 **/ (num_of_int i)))
522

  
520 523
let rec is_eq_const c1 c2 =
521 524
  match c1, c2 with
522 525
  | Const_real (n1, i1, _), Const_real (n2, i2, _)
523
    -> Num.(let n1 = n1 // (num_10 **/ (num_of_int i1)) in
524
	    let n2 = n2 // (num_10 **/ (num_of_int i2)) in
525
	    eq_num n1 n2)
526
    -> let n1 = cst_real_to_num n1 i1 in
527
       let n2 = cst_real_to_num n2 i2 in
528
	    Num.eq_num n1 n2
526 529
  | Const_struct lcl1, Const_struct lcl2
527 530
    -> List.length lcl1 = List.length lcl2
528 531
    && List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2
src/corelang.mli
165 165

  
166 166
val reset_cpt_fresh: unit -> unit
167 167
val mk_fresh_var: node_desc -> Location.t -> Types.type_expr ->  Clocks.clock_expr -> var_decl
168

  
169

  
170
(* Extract a num to describe a real constant *)
171
val cst_real_to_num: Num.num -> int -> Num.num
168 172
(* Local Variables: *)
169 173
(* compile-command:"make -C .." *)
170 174
(* End: *)
src/plugins/salsa/machine_salsa_opt.ml
98 98
    let fresh_id = "toto"  in (* TODO more meaningful name *)
99 99

  
100 100
    let abstractEnv = RangesInt.to_abstract_env ranges in
101
    Format.eprintf "Launching analysis@.@?";
101 102
    let new_e_salsa, e_val = 
102 103
      Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv
103 104
    in
105
    Format.eprintf " Analysis done@.@?";
104 106

  
105 107

  
106 108
    (* (\* Debug *\) *)
......
109 111
    (*   (Salsa.Print.printExpression new_e_salsa); *)
110 112
    (* (\* Debug *\) *)
111 113
    
114
    Format.eprintf " Computing range progress@.@?";
112 115

  
113 116
    let old_val = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in
114 117
    let expr, expr_range  =
......
119 122
	);
120 123
	e_salsa, Some old_val
121 124
      )
122
      | true, false -> (
125
      | false, true -> (
123 126
	if !debug then Log.report ~level:2 (fun fmt ->
124 127
	  Format.fprintf fmt "Improved!@ ";
125 128
	);
126 129
	new_e_salsa, Some e_val
127 130
      )
128
      | false, true -> Format.eprintf "CAREFUL --- new range is worse!. Restoring provided expression@ "; 	e_salsa, Some old_val
129

  
130
      | false, false ->
131
	 Format.eprintf
132
	   "Error; new range is not comparabe with old end. This should not happen!@.@?";
133
	assert false
131
      | true, false -> Format.eprintf "CAREFUL --- new range is worse!. Restoring provided expression@ "; 	e_salsa, Some old_val
132

  
133
      | false, false -> (
134
	Format.eprintf
135
	  "Error; new range is not comparabe with old end. It may need some investigation!@.@?";
136
	Format.eprintf "old: %a@.new: %a@.@?"
137
	  RangesInt.pp_val old_val
138
	  RangesInt.pp_val e_val;
139
	
140
	new_e_salsa, Some e_val
141
       	(* assert false *)
142
      )
134 143
    in
144
    Format.eprintf " Computing range done@.@?";
145

  
135 146
    if !debug then Log.report ~level:2 (fun fmt ->
136 147
      Format.fprintf fmt
137 148
	"  @[<v>old_expr: @[<v 0>%s@ range: %a@]@ new_expr: @[<v 0>%s@ range: %a@]@ @]@ "
src/plugins/salsa/salsaDatatypes.ml
112 112
    | _ -> Format.eprintf "%a cup %a failed@.@?" pp v1 pp v2; assert false 
113 113
*)
114 114
  let inject cst = match cst with  
115
    | LT.Const_int(i)  -> Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_float (float_of_int i))
115
    | LT.Const_int(i)  -> Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_int i)
116 116
    | LT.Const_real (c,e,s) -> (* TODO: this is incorrect. We should rather
117 117
				  compute the error associated to the float *)
118
       let f = float_of_string s  in
119
       Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_float f)
118
       (* let f = float_of_string s in *)
119
       let n = Corelang.cst_real_to_num c e in
120
       Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_num n)
120 121
       
121 122
       (* let r = Salsa.Prelude.r_of_f_aux r in *)
122 123
       (* Salsa.Builder.mk_cst (Float.Domain.nnew r r) *)
......
128 129
      (* 	Salsa.Builder.mk_cst (ST.I(r*.(1.-.epsilon_float),r*.(1.+.epsilon_float)),Float.ulp (ST.I(r,r))) *)
129 130
    | _ -> assert false
130 131

  
131
  let leq = Salsa.Float.feSseq
132
  let leq = (* Salsa.Float.feSseq *) Salsa.Float.Domain.leq
132 133
end
133 134

  
134 135
module RangesInt = Ranges (FloatIntSalsa)

Also available in: Unified diff