Selene/AStat
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Some more debug info

Browse source
This commit is contained in:
Granahir2 2024-06-01 21:46:44 +02:00
parent a422935884
commit 4981194070
1 changed files with 16 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
domains/value_domain.ml
View file

@ -158,8 +158,15 @@ module NonRelational (V : VALUE_DOMAIN) : DOMAIN = struct
let rec revise_HC4 tree mapenv newval = match tree with let rec revise_HC4 tree mapenv newval = match tree with
| HC4_int_unary (uop, sub, abst) -> revise_HC4 sub mapenv (V.bwd_unary (get_abst sub) uop (V.meet abst newval)) | HC4_int_unary (uop, sub, abst) -> revise_HC4 sub mapenv (V.bwd_unary (get_abst sub) uop (V.meet abst newval))
| HC4_int_binary (bop, sub1, sub2, abst) -> let refined1, refined2 = V.bwd_binary (get_abst sub1) (get_abst sub2) bop (V.meet abst newval) in | HC4_int_binary (bop, sub1, sub2, abst) -> let refined1, refined2 = V.bwd_binary (get_abst sub1) (get_abst sub2) bop (V.meet abst newval) in begin
meet (revise_HC4 sub1 mapenv refined1) (revise_HC4 sub2 mapenv refined2) Format.printf "bwd_binary \"%a%s%a = %a\" -> %a, %a@ "
V.print (get_abst sub1)
(Cfg_printer.string_of_int_binary_op bop)
V.print (get_abst sub2)
V.print (V.meet abst newval)
V.print (refined1)
V.print (refined2);
meet (revise_HC4 sub1 mapenv refined1) (revise_HC4 sub2 mapenv refined2) end
| HC4_int_var (v, abst) -> E (VMap.add v (V.meet abst newval) mapenv) | HC4_int_var (v, abst) -> E (VMap.add v (V.meet abst newval) mapenv)
| HC4_int_const (z,abst) -> if( V.is_bottom (V.meet abst newval) ) then Bot else E mapenv | HC4_int_const (z,abst) -> if( V.is_bottom (V.meet abst newval) ) then Bot else E mapenv
| HC4_int_rand (a,b,abst) -> if( V.is_bottom (V.meet abst newval) ) then Bot else E mapenv | HC4_int_rand (a,b,abst) -> if( V.is_bottom (V.meet abst newval) ) then Bot else E mapenv
@ -174,6 +181,13 @@ module NonRelational (V : VALUE_DOMAIN) : DOMAIN = struct
| Bot -> Bot | Bot -> Bot
| E mapenv -> let hc4_1, hc4_2 = build_HC4 iexp1 mapenv, build_HC4 iexp2 mapenv in | E mapenv -> let hc4_1, hc4_2 = build_HC4 iexp1 mapenv, build_HC4 iexp2 mapenv in
let newval1, newval2 = V.compare (get_abst hc4_1) (get_abst hc4_2) cop in ( let newval1, newval2 = V.compare (get_abst hc4_1) (get_abst hc4_2) cop in (
Format.printf "Refined comparison %a%s%a as %a%s%a@ "
V.print (get_abst hc4_1)
(Cfg_printer.string_of_compare_op cop)
V.print (get_abst hc4_2)
V.print newval1
(Cfg_printer.string_of_compare_op cop)
V.print newval2;
meet (revise_HC4 hc4_1 mapenv newval1) (revise_HC4 hc4_2 mapenv newval2) ) meet (revise_HC4 hc4_1 mapenv newval1) (revise_HC4 hc4_2 mapenv newval2) )
let guard env boolexp = guard_noneg env (rm_negations boolexp) let guard env boolexp = guard_noneg env (rm_negations boolexp)