AStat/domains/naked.ml
2024-05-29 11:47:47 +02:00

168 lines
5.7 KiB
OCaml

open Abstract_syntax_tree
open Value_domain
exception NeedTop
exception Absurd
module type NAKED_VALUE_DOMAIN =
sig
type t
val const: Z.t -> t
val rand: Z.t -> Z.t -> t
val minus: t -> t
val binary: t -> t -> int_binary_op -> t
val is_only_zero: t -> bool
val multiples_of: t -> t
val divisors_of: t -> t
val remainders: t -> t
val convex_sym: t -> t
val compatible: t -> compare_op -> t (* returns the arguments possibly on the right of a comp w t*)
val compare: t -> t -> compare_op -> (t*t)
val bwd_binary: t -> t -> int_binary_op -> t -> (t*t)
val join: t -> t -> t
val meet: t -> t -> t
val widen: t -> t -> t
val narrow: t -> t -> t
val subset: t -> t -> bool
val print: Format.formatter -> t -> unit
end
module AddTopBot (N : NAKED_VALUE_DOMAIN) : VALUE_DOMAIN =
struct
type t = Bot | Top | V of N.t
let top = Top
let bottom = Bot
let is_bottom a = match a with
| Bot -> true
| _ -> false
let is_top a = match a with
| Top -> true
| _ -> false
let const c = try V (N.const c) with NeedTop -> Top
let rand a b = try (if Z.equal a b then
V (N.const a)
else (if Z.leq a b then V (N.rand a b) else Bot)) with NeedTop -> Top
let unary a op = try (match op with
| AST_UNARY_PLUS -> a
| AST_UNARY_MINUS -> (match a with
| Top -> Top
| Bot -> Bot
| V t -> V (N.minus t)) ) with NeedTop -> Top
let binary a b op = try( if (is_bottom a || is_bottom b) then (Bot)
else match op with
| AST_PLUS -> if (is_top a || is_top b) then Top else
let V a', V b' = a, b in V (N.binary a' b' AST_PLUS)
| AST_MINUS -> if (is_top a || is_top b) then Top else
let V a', V b' = a, b in V (N.binary a' b' AST_MINUS)
| AST_MULTIPLY -> (match a, b with
| Top, Top -> Top
| Top, V x | V x, Top -> V (N.multiples_of x)
| V x, V y -> V(N.binary x y AST_MULTIPLY))
| AST_DIVIDE -> (match a, b with
| Top, Top -> Top
| Top, V x -> if N.is_only_zero x then Bot else Top
| V x, Top -> V(N.divisors_of x)
| V x, V y -> if N.is_only_zero y then Bot else V(N.binary x y AST_DIVIDE))
| AST_MODULO -> (match a, b with
| Top, Top -> Top
| Top, V x -> if N.is_only_zero x then Bot else V(N.convex_sym x) (* convex symetric hull *)
| V x, Top -> V(N.remainders x)
| V x, V y -> if N.is_only_zero y then Bot else V(N.binary x y AST_MODULO)) ) with NeedTop -> Top
let compare a b op = match a, b with
| Bot, _ | _, Bot -> Bot, Bot
| Top, Top -> Top, Top (* We are non-relational ! *)
| V x, Top -> V x, (try(V (N.compatible x op))with NeedTop->Top)(*We can't learn anything comparing to Top*)
| Top, V x -> (try(V (N.compatible x (reverse op)))with NeedTop->Top), V x
| V x, V y -> try( let a', b' = (N.compare x y op) in V a', V b' )with Absurd -> Bot,Bot
let bwd_unary x op r =
match r with
| Top -> Top
| Bot -> Bot
| V r' -> (match x with
| Top -> (match op with
| AST_UNARY_PLUS -> r
| AST_UNARY_MINUS -> V(N.minus r'))
| Bot -> Bot
| V x' -> (match op with
| AST_UNARY_PLUS -> (try(V (N.meet x' r') )with Absurd -> Bot)
| AST_UNARY_MINUS -> try( V(N.meet x' (N.minus r')))with Absurd->Bot))
let bwd_binary x y op r =
match r with
| Top -> x, y
| Bot -> (match op with
| AST_DIVIDE | AST_MODULO -> x, (try (V (N.const Z.zero) )with NeedTop->Top)
| _ -> x, y (* This can only happen if one of x or y was already Bot *)
)
| V r' -> (match x, y with
| Bot, _| _, Bot -> x,y
| Top, Top -> x, y (*TODO: add some trivialities like a / b = 0 implies a == 0 *)
| V a, Top -> (match op with
| AST_PLUS -> (V a, V (N.binary r' a AST_MINUS))
| AST_MINUS -> (V a, V (N.binary a r' AST_MINUS))
(*
If a can't be null, the values described by b are exactly the values taken by r'/a
(there aren't any rounding issues because r' = ab IMPLIES b = r'/a.)
If a and r' can be null, we can't deduce anything.
If a can be null but r' can't, then b can take any value r'/a can (when a != 0)
*)
| AST_MULTIPLY -> let an, rn = N.subset (N.const Z.zero) a, N.subset (N.const Z.zero) r' in
(match an, rn with
| false, _ -> (V a, V (N.binary r' a AST_DIVIDE))
| true, false -> if N.is_only_zero a then (V a, Bot) else V a, V (N.binary r' a AST_DIVIDE)
| true, true -> (V a, Top))
| AST_DIVIDE | AST_MODULO -> x,y) (* divide has rounding issues, modulo makes my head hurt *)
| Top, V a -> (match op with
| AST_PLUS -> (V (N.binary r' a AST_MINUS), V a)
| AST_MINUS -> (V (N.binary r' a AST_PLUS), V a)
| AST_MULTIPLY -> let an, rn = N.subset (N.const Z.zero) a, N.subset (N.const Z.zero) r' in
(match an, rn with
| false, _ -> (V a, V (N.binary r' a AST_DIVIDE))
| true, false -> if N.is_only_zero a then (V a, Bot) else V a, V (N.binary r' a AST_DIVIDE)
| true, true -> (V a, Top))
| AST_DIVIDE | AST_MODULO -> x,y)
| V a, V b -> try( let a',b' = (N.bwd_binary a b op r') in V a', V b' )with Absurd->(Bot,Bot) )
let join a b = try (match a, b with
| Top, x | x, Top -> Top
| Bot, x | x, Bot -> x
| V a', V b' -> V(N.join a' b') )with NeedTop -> Top
let meet a b = match a, b with
| Bot, x | x, Bot -> Bot
| Top, x | x, Top -> x
| V a', V b' -> try( V(N.meet a' b') )with Absurd -> Bot
let widen a b = try( match a, b with
| Bot, x | x, Bot -> x
| Top, x | x, Top -> Top
| V a', V b' -> V(N.widen a' b') )with NeedTop->Top
let narrow a b = match a, b with
| Bot, x | x, Bot -> Bot
| Top, x | x, Top -> x
| V a', V b' -> try( V(N.narrow a' b') )with Absurd -> Bot
let subset a b = match a, b with
| Bot, b -> true
| b, Bot -> false
| b, Top -> true
| Top, b -> false
| V a', V b' -> (N.subset a' b')
let print out a =
match a with
| Top -> Format.fprintf out "T"
| Bot -> Format.fprintf out "B"
| V a' -> N.print out a'
end