207 lines
7.6 KiB
OCaml
207 lines
7.6 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
|
|
meet (revise_HC4 sub1 mapenv refined1) (revise_HC4 sub2 mapenv refined2)
|
|
| 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 (
|
|
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
|