More work on Salsa plugin

src/corelang.ml

@@ -516,13 +516,16 @@ let sort_handlers hl =
  List.sort (fun (t, _) (t', _) -> compare t t') hl
 
 let num_10 = Num.num_of_int 10
-  
+
+let cst_real_to_num n i =
+  Num.(n // (num_10 **/ (num_of_int i)))
+
 let rec is_eq_const c1 c2 =
   match c1, c2 with
   | Const_real (n1, i1, _), Const_real (n2, i2, _)
-    -> Num.(let n1 = n1 // (num_10 **/ (num_of_int i1)) in
-	    let n2 = n2 // (num_10 **/ (num_of_int i2)) in
-	    eq_num n1 n2)
+    -> let n1 = cst_real_to_num n1 i1 in
+       let n2 = cst_real_to_num n2 i2 in
+	    Num.eq_num n1 n2
   | Const_struct lcl1, Const_struct lcl2
     -> List.length lcl1 = List.length lcl2
     && List.for_all2 (fun (l1, c1) (l2, c2) -> l1 = l2 && is_eq_const c1 c2) lcl1 lcl2

src/corelang.mli

@@ -165,6 +165,10 @@ val expr_contains_expr: tag -> expr -> bool
 
 val reset_cpt_fresh: unit -> unit
 val mk_fresh_var: node_desc -> Location.t -> Types.type_expr ->  Clocks.clock_expr -> var_decl
+
+
+(* Extract a num to describe a real constant *)
+val cst_real_to_num: Num.num -> int -> Num.num
 (* Local Variables: *)
 (* compile-command:"make -C .." *)
 (* End: *)

src/plugins/salsa/machine_salsa_opt.ml

@@ -98,9 +98,11 @@ let opt_num_expr_sliced ranges e_salsa =
     let fresh_id = "toto"  in (* TODO more meaningful name *)
 
     let abstractEnv = RangesInt.to_abstract_env ranges in
+    Format.eprintf "Launching analysis@.@?";
     let new_e_salsa, e_val = 
       Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv
     in
+    Format.eprintf " Analysis done@.@?";
 
 
     (* (\* Debug *\) *)
@@ -109,6 +111,7 @@ let opt_num_expr_sliced ranges e_salsa =
     (*   (Salsa.Print.printExpression new_e_salsa); *)
     (* (\* Debug *\) *)
     
+    Format.eprintf " Computing range progress@.@?";
 
     let old_val = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in
     let expr, expr_range  =
@@ -119,19 +122,27 @@ let opt_num_expr_sliced ranges e_salsa =
 	);
 	e_salsa, Some old_val
       )
-      | true, false -> (
+      | false, true -> (
 	if !debug then Log.report ~level:2 (fun fmt ->
 	  Format.fprintf fmt "Improved!@ ";
 	);
 	new_e_salsa, Some e_val
       )
-      | false, true -> Format.eprintf "CAREFUL --- new range is worse!. Restoring provided expression@ "; 	e_salsa, Some old_val
-
-      | false, false ->
-	 Format.eprintf
-	   "Error; new range is not comparabe with old end. This should not happen!@.@?";
-	assert false
+      | true, false -> Format.eprintf "CAREFUL --- new range is worse!. Restoring provided expression@ "; 	e_salsa, Some old_val
+
+      | false, false -> (
+	Format.eprintf
+	  "Error; new range is not comparabe with old end. It may need some investigation!@.@?";
+	Format.eprintf "old: %a@.new: %a@.@?"
+	  RangesInt.pp_val old_val
+	  RangesInt.pp_val e_val;
+	
+	new_e_salsa, Some e_val
+       	(* assert false *)
+      )
     in
+    Format.eprintf " Computing range done@.@?";
+
     if !debug then Log.report ~level:2 (fun fmt ->
       Format.fprintf fmt
 	"  @[<v>old_expr: @[<v 0>%s@ range: %a@]@ new_expr: @[<v 0>%s@ range: %a@]@ @]@ "

src/plugins/salsa/salsaDatatypes.ml

@@ -112,11 +112,12 @@ struct
     | _ -> Format.eprintf "%a cup %a failed@.@?" pp v1 pp v2; assert false 
 *)
   let inject cst = match cst with  
-    | LT.Const_int(i)  -> Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_float (float_of_int i))
+    | LT.Const_int(i)  -> Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_int i)
     | LT.Const_real (c,e,s) -> (* TODO: this is incorrect. We should rather
 				  compute the error associated to the float *)
-       let f = float_of_string s  in
-       Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_float f)
+       (* let f = float_of_string s in *)
+       let n = Corelang.cst_real_to_num c e in
+       Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_num n)
        
        (* let r = Salsa.Prelude.r_of_f_aux r in *)
        (* Salsa.Builder.mk_cst (Float.Domain.nnew r r) *)
@@ -128,7 +129,7 @@ struct
       (* 	Salsa.Builder.mk_cst (ST.I(r*.(1.-.epsilon_float),r*.(1.+.epsilon_float)),Float.ulp (ST.I(r,r))) *)
     | _ -> assert false
 
-  let leq = Salsa.Float.feSseq
+  let leq = (* Salsa.Float.feSseq *) Salsa.Float.Domain.leq
 end
 
 module RangesInt = Ranges (FloatIntSalsa)