AStat/domains/value_domain.ml
2024-06-09 18:11:53 +02:00

221 lines
8.1 KiB
OCaml

(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
Signature of abstract domains representing sets of integers
(for instance: constants or intervals).
*)
open Abstract_syntax_tree
module type VALUE_DOMAIN =
sig
(* type of abstract elements *)
(* an element of type t abstracts a set of integers *)
type t
(* unrestricted value: [-oo,+oo] *)
val top: t
(* bottom value: empty set *)
val bottom: t
(* constant: {c} *)
val const: Z.t -> t
(* interval: [a,b] *)
val rand: Z.t -> Z.t -> t
(* unary operation *)
val unary: t -> int_unary_op -> t
(* binary operation *)
val binary: t -> t -> int_binary_op -> t
(* comparison *)
(* [compare x y op] returns (x',y') where
- x' abstracts the set of v in x such that v op v' is true for some v' in y
- y' abstracts the set of v' in y such that v op v' is true for some v in x
i.e., we filter the abstract values x and y knowing that the test is true
a safe, but not precise implementation, would be:
compare x y op = (x,y)
*)
val compare: t -> t -> compare_op -> (t * t)
(* backards unary operation *)
(* [bwd_unary x op r] return x':
- x' abstracts the set of v in x such as op v is in r
i.e., we fiter the abstract values x knowing the result r of applying
the operation on x
*)
val bwd_unary: t -> int_unary_op -> t -> t
(* backward binary operation *)
(* [bwd_binary x y op r] returns (x',y') where
- x' abstracts the set of v in x such that v op v' is in r for some v' in y
- y' abstracts the set of v' in y such that v op v' is in r for some v in x
i.e., we filter the abstract values x and y knowing that, after
applying the operation op, the result is in r
*)
val bwd_binary: t -> t -> int_binary_op -> t -> (t * t)
(* set-theoretic operations *)
val join: t -> t -> t
val meet: t -> t -> t
(* widening *)
val widen: t -> t -> t
(* narrowing *)
val narrow: t -> t -> t
(* subset inclusion of concretizations *)
val subset: t -> t -> bool
(* check the emptiness of the concretization *)
val is_bottom: t -> bool
(* print abstract element *)
val print: Format.formatter -> t -> unit
end
open Cfg
open Domain
module NonRelational (V : VALUE_DOMAIN) : DOMAIN = struct
module VMap = VarMap
type t = Bot | E of V.t VMap.t
let init _ = E VMap.empty (* Nonpresent variables are 0 *)
let bottom = Bot
let print out env = match env with
| Bot -> Format.fprintf out "@[<h 0>Bot@]"
| E map -> begin Format.fprintf out "@[<h 0>{";
VMap.iter (fun varid val1 -> Format.fprintf out "%a : %a@ " Cfg_printer.print_var varid V.print val1) map;
Format.fprintf out "}@]"; end
let rec compute e expr = match expr with
| CFG_int_unary (uop, aux) -> V.unary (compute e aux) uop
| CFG_int_binary (bop, aux1, aux2) -> V.binary (compute e aux1) (compute e aux2) bop
| CFG_int_var v -> (try ( VMap.find v e )with Not_found -> V.const Z.zero)
| CFG_int_const c -> V.const c
| CFG_int_rand (c1, c2) -> V.rand c1 c2
let assign env v expr = match env with
| Bot -> Bot
| E envmap -> E (VMap.add v (compute envmap expr) envmap)
let join env1 env2 = match (env1, env2) with
| Bot, x | x, Bot -> x
| E map1, E map2 ->
E (VMap.merge (fun v val1 val2 -> match val1, val2 with
| None, None -> None
| None, Some x | Some x, None -> Some (V.join x (V.const Z.zero))
| Some x, Some y -> Some (V.join x y)) map1 map2)
let meet env1 env2 = match(env1, env2) with
| Bot, x | x, Bot -> Bot
| E map1, E map2 ->
E (VMap.merge (fun v val1 val2 -> match val1, val2 with
| None, None -> None
| None, Some x | Some x, None -> Some (V.meet x (V.const Z.zero))
| Some x, Some y -> Some (V.meet x y)) map1 map2)
type hc4_tree = HC4_int_unary of int_unary_op * hc4_tree * V.t
| HC4_int_binary of int_binary_op * hc4_tree * hc4_tree * V.t
| HC4_int_var of var * V.t
| HC4_int_const of Z.t * V.t
| HC4_int_rand of Z.t*Z.t * V.t
let get_abst hc4 = (match hc4 with
| HC4_int_unary (_,_,v) -> v
| HC4_int_binary (_,_,_,v) -> v
| HC4_int_var (_,v) -> v
| HC4_int_const (_,v) -> v
| HC4_int_rand (_,_,v) -> v)
let rec build_HC4 iexp mapenv = match iexp with
| CFG_int_unary (uop, iexp') -> let sub = build_HC4 iexp' mapenv in HC4_int_unary (uop, sub, (V.unary (get_abst sub) uop))
| CFG_int_binary (bop, iexp1, iexp2) -> let sub1, sub2 = build_HC4 iexp1 mapenv, build_HC4 iexp2 mapenv in
HC4_int_binary (bop,sub1,sub2,(V.binary (get_abst sub1) (get_abst sub2) bop))
| CFG_int_var v -> let abst = (try( VMap.find v mapenv )with Not_found -> V.const Z.zero) in HC4_int_var (v, abst)
| CFG_int_const z -> let abst = V.const z in HC4_int_const (z, abst)
| CFG_int_rand (a, b) -> let abst = V.rand a b in HC4_int_rand (a,b,abst)
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_binary (bop, sub1, sub2, abst) -> let refined1, refined2 = V.bwd_binary (get_abst sub1) (get_abst sub2) bop (V.meet abst newval) in begin
(*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_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
let rec guard_noneg env boolexp = match boolexp with
| CFG_bool_unary (_, _) -> failwith "We were supposed to remove negations !!"
| CFG_bool_binary (AST_AND, exp1, exp2) -> meet (guard_noneg env exp1) (guard_noneg env exp2)
| CFG_bool_binary (AST_OR, exp1, exp2) -> join (guard_noneg env exp1) (guard_noneg env exp2)
| CFG_bool_const (b) -> if b then env else Bot
| CFG_bool_rand -> env
| CFG_compare (cop, iexp1, iexp2) -> match env with
| Bot -> Bot
| 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 (
(*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) )
let guard env boolexp = guard_noneg env (rm_negations boolexp)
let widen env1 env2 = match (env1, env2) with
| Bot, x | x, Bot -> x
| E map1, E map2 ->
E (VMap.merge (fun v val1 val2 -> match val1, val2 with
| None, None -> None
| None, Some x | Some x, None -> Some (V.widen x (V.const Z.zero))
| Some x, Some y -> Some (V.widen x y)) map1 map2)
let narrow env1 env2 = match(env1, env2) with
| Bot, x | x, Bot -> Bot
| E map1, E map2 ->
E (VMap.merge (fun v val1 val2 -> match val1, val2 with
| None, None -> None
| None, Some x | Some x, None -> Some (V.narrow x (V.const Z.zero))
| Some x, Some y -> Some (V.narrow x y)) map1 map2)
let subset env1 env2 = match env1, env2 with
| Bot, _ -> true
| _, Bot -> false
| E map1, E map2 -> let b1 = VMap.for_all (fun varid val1 -> match VMap.find_opt varid map2 with
| None -> V.subset val1 (V.const Z.zero)
| Some val2 -> V.subset val1 val2) map1 in
let b2 = VMap.for_all (fun varid val2 -> match VMap.find_opt varid map1 with
| None -> V.subset (V.const Z.zero) val2
| Some val1 -> V.subset val1 val2) map2 in
b1 && b2
let is_bottom env = match env with
| Bot -> true
| E map -> VMap.exists (fun varid val1 -> V.is_bottom val1) map
end