### Profile

« Previous | Next »

## Revision 9a9058f4

#### Added by Pierre-Loïc Garocheover 5 years ago

More work on Salsa plugin

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@]@ @]@ "
```
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