Project

General

Profile

« Previous | Next » 

Revision 94c457b7

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

Updated Salsa plugin to latest version of Salsa.
Some issues wrt machine type features.
Work in progress

View differences:

src/plugins/salsa/salsaDatatypes.ml
1 1 
module LT = LustreSpec
2 2 
module MC = Machine_code
3 
module ST = Salsa.SalsaTypes
3 
module ST = Salsa.Types
4 4 
module Float = Salsa.Float
5 5 

  		




  6
  
  
    
let debug = true


  		




  
  6
  
    
let debug = ref false


  		




  7
  7
  
    

  		




  8
  8
  
    
let pp_hash ~sep f fmt r = 


  		




  9
  9
  
    
  Format.fprintf fmt "[@[<v>";


  		




  ......




  108
  108
  
    
struct


  		




  109
  109
  
    
  type t = ST.abstractValue


  		




  110
  110
  
    

  		




  111
  
  
    
  let pp fmt (f,r) = 


  		




  112
  
  
    
    match f, r with


  		




  
  111
  
    
  let pp fmt (f,r) =


  		




  
  112
  
    
    let fs, rs = (Salsa.Float.Domain.print (f,r)) in


  		




  
  113
  
    
    Format.fprintf fmt "%s + %s" fs rs 


  		




  
  114
  
    
(*    match f, r with


  		




  113
  115
  
    
    | ST.I(a,b), ST.J(c,d) ->


  		




  114
  
  
    
      Format.fprintf fmt "[%f, %f] + [%f, %f]" a b c d


  		




  
  116
  
    
      Format.fprintf fmt "[%f, %f] + [%s, %s]" a b (Num.string_of_num c) (Num.string_of_num d)


  		




  115
  117
  
    
    | ST.I(a,b), ST.JInfty ->  Format.fprintf fmt "[%f, %f] + oo" a b 


  		




  116
  118
  
    
    | ST.Empty, _ -> Format.fprintf fmt "???"


  		




  117
  119
  
    

  		




  118
  120
  
    
    | _ -> assert false


  		




  119
  
  
    

  		




  120
  
  
    
  let union v1 v2 = 


  		




  121
  
  
    
    match v1, v2 with


  		




  
  121
  
    
*)


  		




  
  122
  
    
  let union v1 v2 = Salsa.Float.Domain.join v1 v2


  		




  
  123
  
    
(*    match v1, v2 with


  		




  122
  124
  
    
    |(ST.I(x1, x2), ST.J(y1, y2)), (ST.I(x1', x2'), ST.J(y1', y2')) ->


  		




  123
  125
  
    
      ST.(I(min x1 x1', max x2 x2'), J(min y1 y1', max y2 y2'))


  		




  124
  126
  
    
    | _ -> Format.eprintf "%a cup %a failed@.@?" pp v1 pp v2; assert false 


  		




  125
  
  
    

  		




  
  127
  
    
*)


  		




  126
  128
  
    
  let inject cst = match cst with


  		




  127
  
  
    
    | LT.Const_int(i)  -> Salsa.Builder.mk_cst (ST.I(float_of_int i,float_of_int i),ST.J(0.0,0.0))


  		




  
  129
  
    
    | LT.Const_int(i)  -> Salsa.Builder.mk_cst (ST.R(Num.num_of_int i, []), ST.R(Num.num_of_int i, []))


  		




  128
  130
  
    
    | LT.Const_real (c,e,s) -> (* TODO: this is incorrect. We should rather


  		




  129
  131
  
    
				  compute the error associated to the float *)


  		




  130
  
  
    
      let r = float_of_string s  in


  		




  131
  
  
    
      if r = 0. then


  		




  132
  
  
    
	Salsa.Builder.mk_cst (ST.I(-. min_float, min_float),Float.ulp (ST.I(-. min_float, min_float)))


  		




  133
  
  
    
      else


  		




  134
  
  
    
	Salsa.Builder.mk_cst (ST.I(r*.(1.-.epsilon_float),r*.(1.+.epsilon_float)),Float.ulp (ST.I(r,r)))


  		




  
  132
  
    
       


  		




  
  133
  
    
       let r = float_of_string s  in


  		




  
  134
  
    
       let r = Salsa.Prelude.r_of_f_aux r in


  		




  
  135
  
    
       Salsa.Builder.mk_cst (Float.Domain.nnew r r)


  		




  
  136
  
    
	 


  		




  
  137
  
    
      (* let r = float_of_string s  in *)


  		




  
  138
  
    
      (* if r = 0. then *)


  		




  
  139
  
    
      (* 	Salsa.Builder.mk_cst (ST.R(-. min_float, min_float),Float.ulp (ST.R(-. min_float, min_float))) *)


  		




  
  140
  
    
      (* else *)


  		




  
  141
  
    
      (* 	Salsa.Builder.mk_cst (ST.I(r*.(1.-.epsilon_float),r*.(1.+.epsilon_float)),Float.ulp (ST.I(r,r))) *)


  		




  135
  142
  
    
    | _ -> assert false


  		




  136
  143
  
    
end


  		




  137
  144
  
    

  		




  ......




  258
  265
  
    
    MC.mk_val (LT.Fun (op, [x;y])) t


  		




  259
  266
  
    
  in


  		




  260
  267
  
    
  match e with


  		




  261
  
  
    
    ST.Cst((ST.I(f1,f2),_),_)     -> (* We project ranges into constants. We


  		




  
  268
  
    
    ST.Cst((ST.R(c,_),_),_)     -> (* We project ranges into constants. We


  		




  262
  269
  
    
					forget about errors and provide the


  		




  263
  270
  
    
					mean/middle value of the interval


  		




  264
  271
  
    
				     *)


  		




  265
  
  
    
      let new_float = 


  		




  266
  
  
    
	if f1 = f2 then


  		




  267
  
  
    
	  f1


  		




  268
  
  
    
	else


  		




  269
  
  
    
	  (f1 +. f2) /. 2.0 


  		




  270
  
  
    
      in


  		




  271
  
  
    
      Log.report ~level:3


  		




  272
  
  
    
	(fun fmt -> Format.fprintf fmt  "projecting [%.45f, %.45f] -> %.45f@ " f1 f2 new_float);


  		




  
  272
  
    
      let  new_float = Num.float_of_num c in


  		




  
  273
  
    
      (* let new_float =  *)


  		




  
  274
  
    
      (* 	if f1 = f2 then *)


  		




  
  275
  
    
      (* 	  f1 *)


  		




  
  276
  
    
      (* 	else *)


  		




  
  277
  
    
      (* 	  (f1 +. f2) /. 2.0  *)


  		




  
  278
  
    
      (* in *)


  		




  
  279
  
    
      (* Log.report ~level:3 *)


  		




  
  280
  
    
      (* 	(fun fmt -> Format.fprintf fmt  "projecting [%.45f, %.45f] -> %.45f@ " f1 f2 new_float); *)


  		




  273
  281
  
    
      let cst =  


  		




  274
  282
  
    
	let s = 


  		




  275
  283
  
    
	  if new_float = 0. then "0." else


  		












Also available in:  Unified diff