Skip to content

Commit

Permalink
Merge pull request #1329 from goblint/z-module
Browse files Browse the repository at this point in the history 
Use Z module directly
  • Loading branch information
@sim642
sim642 authored Jan 29, 2024
2 parents a495645 + 67320d4 commit 9178c43
Show file tree
Hide file tree
Showing 20 changed files with 583 additions and 592 deletions.
47 changes: 23 additions & 24 deletions src/analyses/base.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,6 @@ module Addr = ValueDomain.Addr
module Offs = ValueDomain.Offs
module LF = LibraryFunctions
module CArrays = ValueDomain.CArrays
module BI = IntOps.BigIntOps
module PU = PrecisionUtil

module VD = BaseDomain.VD
Expand Down Expand Up @@ -174,8 +173,8 @@ struct

let unop_ID = function
| Neg -> ID.neg
| BNot -> ID.bitnot
| LNot -> ID.lognot
| BNot -> ID.lognot
| LNot -> ID.c_lognot

let unop_FD = function
| Neg -> FD.neg
Expand Down Expand Up @@ -213,13 +212,13 @@ struct
evalint: base eval_rv 1 -> (1,[1,1])
evalint: base query_evalint m == 1 -> (0,[1,1]) *)
| Ne -> ID.ne
| BAnd -> ID.bitand
| BOr -> ID.bitor
| BXor -> ID.bitxor
| BAnd -> ID.logand
| BOr -> ID.logor
| BXor -> ID.logxor
| Shiftlt -> ID.shift_left
| Shiftrt -> ID.shift_right
| LAnd -> ID.logand
| LOr -> ID.logor
| LAnd -> ID.c_logand
| LOr -> ID.c_logor
| b -> (fun x y -> (ID.top_of result_ik))

let binop_FD (result_fk: Cil.fkind) = function
Expand Down Expand Up @@ -247,7 +246,7 @@ struct
if M.tracing then M.tracel "eval" "evalbinop %a %a %a\n" d_binop op VD.pretty a1 VD.pretty a2;
(* We define a conversion function for the easy cases when we can just use
* the integer domain operations. *)
let bool_top ik = ID.(join (of_int ik BI.zero) (of_int ik BI.one)) in
let bool_top ik = ID.(join (of_int ik Z.zero) (of_int ik Z.one)) in
(* An auxiliary function for ptr arithmetic on array values. *)
let addToAddr n (addr:Addr.t) =
let typeOffsetOpt o t =
Expand All @@ -270,7 +269,7 @@ struct
begin match t with
| Some t ->
let (f_offset_bits, _) = bitsOffset t (Field (f, NoOffset)) in
let f_offset = IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) (BI.of_int (f_offset_bits / 8)) in
let f_offset = IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int (f_offset_bits / 8)) in
begin match IdxDom.(to_bool (eq f_offset (neg n_offset))) with
| Some true -> `NoOffset
| _ -> `Field (f, `Index (n_offset, `NoOffset))
Expand All @@ -286,7 +285,7 @@ struct
| `NoOffset -> `Index(iDtoIdx n, `NoOffset)
in
let default = function
| Addr.NullPtr when GobOption.exists (BI.equal BI.zero) (ID.to_int n) -> Addr.NullPtr
| Addr.NullPtr when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> Addr.NullPtr
| _ -> Addr.UnknownPtr
in
match Addr.to_mval addr with
Expand Down Expand Up @@ -388,9 +387,9 @@ struct
Int (ID.top_of ik)
end
| Eq ->
Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.zero else match eq p1 p2 with Some x when x -> ID.of_int ik BI.one | _ -> bool_top ik)
Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik Z.zero else match eq p1 p2 with Some x when x -> ID.of_int ik Z.one | _ -> bool_top ik)
| Ne ->
Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.one else match eq p1 p2 with Some x when x -> ID.of_int ik BI.zero | _ -> bool_top ik)
Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik Z.one else match eq p1 p2 with Some x when x -> ID.of_int ik Z.zero | _ -> bool_top ik)
| IndexPI when AD.to_string p2 = ["all_index"] ->
addToAddrOp p1 (ID.top_of (Cilfacade.ptrdiff_ikind ()))
| IndexPI | PlusPI ->
Expand Down Expand Up @@ -872,7 +871,7 @@ struct
(* CIL's very nice implicit conversion of an array name [a] to a pointer
* to its first element [&a[0]]. *)
| StartOf lval ->
let array_ofs = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset) in
let array_ofs = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset) in
let array_start = add_offset_varinfo array_ofs in
Address (AD.map array_start (eval_lv ~ctx st lval))
| CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~ctx st (Const (CStr (x,e))) (* TODO safe? *)
Expand Down Expand Up @@ -975,11 +974,11 @@ struct
match op with
| MinusA when must_be_equal () ->
let ik = Cilfacade.get_ikind t in
Int (ID.of_int ik BI.zero)
Int (ID.of_int ik Z.zero)
| MinusPI (* TODO: untested *)
| MinusPP when must_be_equal () ->
let ik = Cilfacade.ptrdiff_ikind () in
Int (ID.of_int ik BI.zero)
Int (ID.of_int ik Z.zero)
(* Eq case is unnecessary: Q.must_be_equal reconstructs BinOp (Eq, _, _, _) and repeats EvalInt query for that, yielding a top from query cycle and never being must equal *)
| Le
| Ge when must_be_equal () ->
Expand Down Expand Up @@ -1272,7 +1271,7 @@ struct
| _ -> None
in
let alen = Seq.filter_map (fun v -> lenOf v.vtype) (List.to_seq (AD.to_var_may a)) in
let d = Seq.fold_left ID.join (ID.bot_of (Cilfacade.ptrdiff_ikind ())) (Seq.map (ID.of_int (Cilfacade.ptrdiff_ikind ()) %BI.of_int) (Seq.append slen alen)) in
let d = Seq.fold_left ID.join (ID.bot_of (Cilfacade.ptrdiff_ikind ())) (Seq.map (ID.of_int (Cilfacade.ptrdiff_ikind ()) %Z.of_int) (Seq.append slen alen)) in
(* ignore @@ printf "EvalLength %a = %a\n" d_exp e ID.pretty d; *)
`Lifted d
| Bot -> Queries.Result.bot q (* TODO: remove *)
Expand Down Expand Up @@ -1305,7 +1304,7 @@ struct
(match r with
| Array a ->
(* unroll into array for Calloc calls *)
(match ValueDomain.CArrays.get (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) a (None, (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero)) with
(match ValueDomain.CArrays.get (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) a (None, (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero)) with
| Blob (_,s,_) -> `Lifted s
| _ -> Queries.Result.top q
)
Expand Down Expand Up @@ -2455,7 +2454,7 @@ struct
| Isgreaterequal (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.ge x y))
| Isless (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.lt x y))
| Islessequal (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.le x y))
| Islessgreater (x,y) -> Int(ID.logor (ID.cast_to IInt (apply_binary FDouble FD.lt x y)) (ID.cast_to IInt (apply_binary FDouble FD.gt x y)))
| Islessgreater (x,y) -> Int(ID.c_logor (ID.cast_to IInt (apply_binary FDouble FD.lt x y)) (ID.cast_to IInt (apply_binary FDouble FD.gt x y)))
| Isunordered (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.unordered x y))
| Fmax (fd, x ,y) -> Float (apply_binary fd FD.fmax x y)
| Fmin (fd, x ,y) -> Float (apply_binary fd FD.fmin x y)
Expand All @@ -2475,7 +2474,7 @@ struct
let st' =
(* TODO: should invalidate shallowly? https://github.com/goblint/analyzer/pull/1224#discussion_r1405826773 *)
match eval_rv ~ctx st ret_var with
| Int n when GobOption.exists (BI.equal BI.zero) (ID.to_int n) -> st
| Int n when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> st
| Address ret_a ->
begin match eval_rv ~ctx st id with
| Thread a when ValueDomain.Threads.is_top a -> invalidate ~ctx st [ret_var]
Expand Down Expand Up @@ -2535,8 +2534,8 @@ struct
let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in
(* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)
set_many ~ctx st [
(add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (Blob (VD.bot (), blobsize, false))));
(eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))
(add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.one) (Blob (VD.bot (), blobsize, false))));
(eval_lv ~ctx st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset)))))
]
)
| _ -> st
Expand All @@ -2551,7 +2550,7 @@ struct
match p_rv with
| Address a -> a
(* TODO: don't we already have logic for this? *)
| Int i when ID.to_int i = Some BI.zero -> AD.null_ptr
| Int i when ID.to_int i = Some Z.zero -> AD.null_ptr
| Int i -> AD.top_ptr
| _ -> AD.top_ptr (* TODO: why does this ever happen? *)
in
Expand Down Expand Up @@ -2590,7 +2589,7 @@ struct
in
begin match lv with
| Some lv ->
set ~ctx st' (eval_lv ~ctx st lv) (Cilfacade.typeOfLval lv) (Int (ID.of_int IInt BI.zero))
set ~ctx st' (eval_lv ~ctx st lv) (Cilfacade.typeOfLval lv) (Int (ID.of_int IInt Z.zero))
| None -> st'
end
| Longjmp {env; value}, _ ->
Expand Down
53 changes: 25 additions & 28 deletions src/analyses/baseInvariant.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module VD = BaseDomain.VD
module ID = ValueDomain.ID
module FD = ValueDomain.FD
module AD = ValueDomain.AD
module BI = IntOps.BigIntOps

module type Eval =
sig
Expand Down Expand Up @@ -44,8 +43,8 @@ struct

let unop_ID = function
| Neg -> ID.neg
| BNot -> ID.bitnot
| LNot -> ID.lognot
| BNot -> ID.lognot
| LNot -> ID.c_lognot

let unop_FD = function
| Neg -> FD.neg
Expand Down Expand Up @@ -140,7 +139,7 @@ struct
match ID.to_int n with
| Some n ->
(* When x != n, we can return a singleton exclusion set *)
if M.tracing then M.tracec "invariant" "Yes, %a is not %s\n" d_lval x (BI.to_string n);
if M.tracing then M.tracec "invariant" "Yes, %a is not %a\n" d_lval x GobZ.pretty n;
let ikind = Cilfacade.get_ikind_exp (Lval lval) in
Some (x, Int (ID.of_excl_list ikind [n]))
| None -> None
Expand Down Expand Up @@ -169,11 +168,11 @@ struct
| Int n -> begin
let ikind = Cilfacade.get_ikind_exp (Lval lval) in
let n = ID.cast_to ikind n in
let range_from x = if tv then ID.ending ikind (BI.sub x BI.one) else ID.starting ikind x in
let range_from x = if tv then ID.ending ikind (Z.pred x) else ID.starting ikind x in
let limit_from = if tv then ID.maximal else ID.minimal in
match limit_from n with
| Some n ->
if M.tracing then M.tracec "invariant" "Yes, success! %a is not %s\n\n" d_lval x (BI.to_string n);
if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a\n\n" d_lval x GobZ.pretty n;
Some (x, Int (range_from n))
| None -> None
end
Expand All @@ -184,11 +183,11 @@ struct
| Int n -> begin
let ikind = Cilfacade.get_ikind_exp (Lval lval) in
let n = ID.cast_to ikind n in
let range_from x = if tv then ID.ending ikind x else ID.starting ikind (BI.add x BI.one) in
let range_from x = if tv then ID.ending ikind x else ID.starting ikind (Z.succ x) in
let limit_from = if tv then ID.maximal else ID.minimal in
match limit_from n with
| Some n ->
if M.tracing then M.tracec "invariant" "Yes, success! %a is not %s\n\n" d_lval x (BI.to_string n);
if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a\n\n" d_lval x GobZ.pretty n;
Some (x, Int (range_from n))
| None -> None
end
Expand All @@ -205,7 +204,7 @@ struct
match Cil.unrollType typ with
| TPtr _ -> Address AD.null_ptr
| TEnum({ekind=_;_},_)
| _ -> Int (ID.of_int (Cilfacade.get_ikind typ) BI.zero)
| _ -> Int (ID.of_int (Cilfacade.get_ikind typ) Z.zero)
in
let rec derived_invariant exp tv =
let switchedOp = function Lt -> Gt | Gt -> Lt | Le -> Ge | Ge -> Le | x -> x in (* a op b <=> b (switchedOp op) b *)
Expand Down Expand Up @@ -255,7 +254,7 @@ struct
(* ikind is the type of a for limiting ranges of the operands a, b. The only binops which can have different types for a, b are Shiftlt, Shiftrt (not handled below; don't use ikind to limit b there). *)
let inv_bin_int (a, b) ikind c op =
let warn_and_top_on_zero x =
if GobOption.exists (BI.equal BI.zero) (ID.to_int x) then
if GobOption.exists (Z.equal Z.zero) (ID.to_int x) then
(M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top";
ID.top_of ikind)
else
Expand All @@ -278,7 +277,7 @@ struct
(* refine x by information about y, using x * y == c *)
let refine_by x y = (match ID.to_int y with
| None -> x
| Some v when BI.equal (BI.rem v (BI.of_int 2)) BI.zero (* v % 2 = 0 *) -> x (* A refinement would still be possible here, but has to take non-injectivity into account. *)
| Some v when Z.equal (Z.rem v (Z.of_int 2)) Z.zero (* v % 2 = 0 *) -> x (* A refinement would still be possible here, but has to take non-injectivity into account. *)
| Some v (* when Int64.rem v 2L = 1L *) -> id_meet_down ~old:x ~c:(ID.div c y)) (* Div is ok here, c must be divisible by a and b *)
in
(refine_by a b, refine_by b a)
Expand All @@ -290,11 +289,11 @@ struct
* However, a%b will give [-b+1, b-1] for a=top, but we only want the positive/negative side depending on the sign of c*b.
* If c*b = 0 or it can be positive or negative, we need the full range for the remainder. *)
let rem =
let is_pos = ID.to_bool @@ ID.gt (ID.mul b c) (ID.of_int ikind BI.zero) = Some true in
let is_neg = ID.to_bool @@ ID.lt (ID.mul b c) (ID.of_int ikind BI.zero) = Some true in
let is_pos = ID.to_bool @@ ID.gt (ID.mul b c) (ID.of_int ikind Z.zero) = Some true in
let is_neg = ID.to_bool @@ ID.lt (ID.mul b c) (ID.of_int ikind Z.zero) = Some true in
let full = ID.rem a b in
if is_pos then ID.meet (ID.starting ikind BI.zero) full
else if is_neg then ID.meet (ID.ending ikind BI.zero) full
if is_pos then ID.meet (ID.starting ikind Z.zero) full
else if is_neg then ID.meet (ID.ending ikind Z.zero) full
else full
in
meet_bin (ID.add (ID.mul b c) rem) (ID.div (ID.sub a rem) c)
Expand All @@ -310,11 +309,11 @@ struct
* If b is negative we have to look at the lower bound. *)
let is_divisible bound =
match bound a with
| Some ba -> ID.rem (ID.of_int ikind ba) b |> ID.to_int = Some BI.zero
| Some ba -> ID.rem (ID.of_int ikind ba) b |> ID.to_int = Some Z.zero
| None -> false
in
let max_pos = match ID.maximal b with None -> true | Some x -> BI.compare x BI.zero >= 0 in
let min_neg = match ID.minimal b with None -> true | Some x -> BI.compare x BI.zero < 0 in
let max_pos = match ID.maximal b with None -> true | Some x -> Z.compare x Z.zero >= 0 in
let min_neg = match ID.minimal b with None -> true | Some x -> Z.compare x Z.zero < 0 in
let implies a b = not a || b in
let a'' =
if implies max_pos (is_divisible ID.maximal) && implies min_neg (is_divisible ID.minimal) then
Expand All @@ -333,10 +332,10 @@ struct
let a,b = meet_bin a''' b' in
(* Special handling for case a % 2 != c *)
let a = if PrecisionUtil.(is_congruence_active (int_precision_from_node_or_config ())) then
let two = BI.of_int 2 in
let two = Z.of_int 2 in
match ID.to_int b, ID.to_excl_list c with
| Some b, Some ([v], _) when BI.equal b two ->
let k = if BI.equal (BI.abs (BI.rem v two)) (BI.zero) then BI.one else BI.zero in
| Some b, Some ([v], _) when Z.equal b two ->
let k = if Z.equal (Z.abs (Z.rem v two)) Z.zero then Z.one else Z.zero in
ID.meet (ID.of_congruence ikind (k, b)) a
| _, _ -> a
else a
Expand Down Expand Up @@ -381,8 +380,6 @@ struct
| _, _ -> a, b
end
| Lt | Le | Ge | Gt as op ->
let pred x = BI.sub x BI.one in
let succ x = BI.add x BI.one in
(match ID.minimal a, ID.maximal a, ID.minimal b, ID.maximal b with
| Some l1, Some u1, Some l2, Some u2 ->
(* if M.tracing then M.tracel "inv" "Op: %s, l1: %Ld, u1: %Ld, l2: %Ld, u2: %Ld\n" (show_binop op) l1 u1 l2 u2; *)
Expand All @@ -396,9 +393,9 @@ struct
| Ge, Some true
| Lt, Some false -> meet_bin (ID.starting ikind l2) (ID.ending ikind u1)
| Lt, Some true
| Ge, Some false -> meet_bin (ID.ending ikind (pred u2)) (ID.starting ikind (succ l1))
| Ge, Some false -> meet_bin (ID.ending ikind (Z.pred u2)) (ID.starting ikind (Z.succ l1))
| Gt, Some true
| Le, Some false -> meet_bin (ID.starting ikind (succ l2)) (ID.ending ikind (pred u1))
| Le, Some false -> meet_bin (ID.starting ikind (Z.succ l2)) (ID.ending ikind (Z.pred u1))
| _, _ -> a, b)
| _ -> a, b)
| BOr | BXor as op->
Expand All @@ -414,7 +411,7 @@ struct
(* we only attempt to refine a here *)
let a =
match ID.to_int b with
| Some x when BI.equal x BI.one ->
| Some x when Z.equal x Z.one ->
(match ID.to_bool c with
| Some true -> ID.meet a (ID.of_congruence ikind (Z.one, Z.of_int 2))
| Some false -> ID.meet a (ID.of_congruence ikind (Z.zero, Z.of_int 2))
Expand Down Expand Up @@ -574,7 +571,7 @@ struct
| Some true ->
(* i.e. e should evaluate to [1,1] *)
(* LNot x is 0 for any x != 0 *)
ID.of_excl_list ikind [BI.zero]
ID.of_excl_list ikind [Z.zero]
| Some false -> ID.of_bool ikind false
| _ -> ID.top_of ikind
in
Expand Down Expand Up @@ -810,7 +807,7 @@ struct
let itv = if not tv || is_cmp exp then (* false is 0, but true can be anything that is not 0, except for comparisons which yield 1 *)
ID.of_bool ik tv (* this will give 1 for true which is only ok for comparisons *)
else
ID.of_excl_list ik [BI.zero] (* Lvals, Casts, arithmetic operations etc. should work with true = non_zero *)
ID.of_excl_list ik [Z.zero] (* Lvals, Casts, arithmetic operations etc. should work with true = non_zero *)
in
inv_exp (Int itv) exp st
| exception Invalid_argument _ ->
Expand Down
Loading

0 comments on commit 9178c43

Please sign in to comment.