Skip to content

Commit 355348f

Browse files
FungOliverFungOliver
committed
simplify query logic
1 parent 4b1b6fa commit 355348f

File tree

3 files changed

+66
-86
lines changed

3 files changed

+66
-86
lines changed

‎src/analyses/apron/relationAnalysis.apron.ml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -862,13 +862,13 @@ struct
862862
| Queries.Invariant context -> query_invariant ctx context
863863

864864
(* the lval arr has the length of the arr we now want to check if the expression index is within the bounds of arr please use relational Analysis *)
865-
| Queries.MayBeOutOfBounds (v ,t ,exp) ->
866-
let newVar = ArrayMap.to_varinfo (v, t) in
865+
| Queries.MayBeOutOfBounds {var= v ;dimension = d ;index =exp} ->
866+
let newVar = ArrayMap.to_varinfo (v, d) in
867867
let comp = Cilfacade.makeBinOp Lt exp (Lval (Var newVar,NoOffset)) in
868868
let i = eval_int comp (no_overflow ask comp ) in
869869
if M.tracing then M.trace "relationalArray" "comp: %a\n result=%a" d_exp comp ID.pretty i;
870870
i
871-
| AllocMayBeOutOfBounds (e, i, o, _) ->
871+
| AllocMayBeOutOfBounds {exp=e;e1_offset= i;struct_offset= o; _} ->
872872
let inBoundsForAllAddresses indexExp = begin match ctx.ask (Queries.MayPointTo e) with
873873
| a when not (Queries.AD.is_top a) ->
874874
Queries.AD.fold ( fun (addr : AD.elt) (st ) ->

‎src/analyses/memOutOfBounds.ml‎

Lines changed: 52 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -291,7 +291,7 @@ struct
291291
ID.cast_to (Cilfacade.ptrdiff_ikind ()) offs_intdom, offsetTyp
292292
end
293293
in
294-
let isAfterZero, isBeforeEnd = (ctx.ask (Queries.AllocMayBeOutOfBounds (e, addr_offs_casted, structOffset, currentSizeTyp))) in
294+
let isAfterZero, isBeforeEnd = (ctx.ask (Queries.AllocMayBeOutOfBounds {exp=e;e1_offset= addr_offs_casted;struct_offset= structOffset;offset_typ= currentSizeTyp})) in
295295
let isAfterZeroBool, isBeforeEndBool = (VDQ.ID.to_bool isAfterZero, VDQ.ID.to_bool isBeforeEnd) in
296296
begin match isAfterZeroBool with
297297
| None ->
@@ -435,61 +435,61 @@ struct
435435

436436
let query ctx (type a) (q: a Queries.t): a Queries.result =
437437
match q with
438-
| Queries.AllocMayBeOutOfBounds (e, i, o, t) ->
438+
| Queries.AllocMayBeOutOfBounds {exp=e;e1_offset= i;struct_offset= o; offset_typ = t} ->
439439
begin match i with
440440
| i when not @@ ID.is_bot i ->
441-
if M.tracing then M.trace "OOB" "e=%a i=%a o=%a\n" d_exp e ID.pretty i ID.pretty o;
442-
let expOffset = match e with
443-
| Lval (Var v, _) -> i
444-
| BinOp (binop, e1, e2, t) when binop = PlusPI || binop = IndexPI || binop = MinusPI ->
445-
let ptr_deref_type = get_ptr_deref_type @@ typeOf e1 in
446-
begin match ptr_deref_type with
447-
| Some typ->
448-
let e2Offset = eval_ptr_offset_in_binop ctx e2 typ in (*add offset of e2*)
449-
begin match e2Offset with
450-
| `Lifted e2Offset ->
451-
begin
452-
try if binop = MinusPI then
453-
ID.sub i e2Offset
454-
else
455-
ID.add i e2Offset
456-
with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of (Cilfacade.ptrdiff_ikind ())
457-
end
458-
| `Top | `Bot -> ID.top_of (Cilfacade.ptrdiff_ikind ())
441+
if M.tracing then M.trace "OOB" "e=%a i=%a o=%a\n" d_exp e ID.pretty i ID.pretty o;
442+
let expOffset = match e with
443+
| Lval (Var v, _) -> i
444+
| BinOp (binop, e1, e2, t) when binop = PlusPI || binop = IndexPI || binop = MinusPI ->
445+
let ptr_deref_type = get_ptr_deref_type @@ typeOf e1 in
446+
begin match ptr_deref_type with
447+
| Some typ->
448+
let e2Offset = eval_ptr_offset_in_binop ctx e2 typ in (*add offset of e2*)
449+
begin match e2Offset with
450+
| `Lifted e2Offset ->
451+
begin
452+
try if binop = MinusPI then
453+
ID.sub i e2Offset
454+
else
455+
ID.add i e2Offset
456+
with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of (Cilfacade.ptrdiff_ikind ())
459457
end
460-
| _ -> ID.top_of (Cilfacade.ptrdiff_ikind ())
458+
| `Top | `Bot -> ID.top_of (Cilfacade.ptrdiff_ikind ())
461459
end
462-
| _ ->failwith "unexpected expression in query AllocMayBeOutOfBounds \n"
463-
in
464-
if M.tracing then M.trace "OOB" "e=%a expOffset %a \n" d_exp e ID.pretty expOffset;
465-
let isBeforeZero = ID.le (ID.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero) expOffset in (*check for negative Indices*)
466-
467-
let currentTypSize = size_of_type_in_bytes t in
468-
let castedCurrentTypSize = ID.cast_to (Cilfacade.ptrdiff_ikind ()) currentTypSize in (*add size of type*)
469-
let expOffset_CurrentTyPSize =
470-
begin try ID.add expOffset castedCurrentTypSize
471-
with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of (Cilfacade.ptrdiff_ikind ())
472-
end
473-
in
474-
if M.tracing then M.trace "OOB" "current_index_size %a \n" ID.pretty currentTypSize;
475-
if M.tracing then M.trace "OOB" "expOffset_plus_current_index_size %a \n" ID.pretty expOffset_CurrentTyPSize;
476-
let expOffset_CurrentTypSize_StructOffset =
477-
(try (ID.add o expOffset_CurrentTyPSize)
478-
with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of (Cilfacade.ptrdiff_ikind ()))
479-
in
480-
if M.tracing then M.trace "OOB" "exp_Offset_plus_current_index_size_struct_offset %a \n" ID.pretty expOffset_CurrentTypSize_StructOffset;
481-
let isBeforeEnd = match get_size_of_ptr_target ctx e with
482-
| `Lifted size ->
483-
let casted_e_size = ID.cast_to (Cilfacade.ptrdiff_ikind ()) size in
484-
if M.tracing then M.trace "OOB" "casted_e_size %a \n" ID.pretty casted_e_size;
485-
ID.le expOffset_CurrentTypSize_StructOffset casted_e_size
486-
| `Top -> ID.top_of IInt
487-
| `Bot -> ID.top_of IInt (*Ikind of ID comparisons*)
488-
in
489-
if M.tracing then M.trace "OOB" "result %a %a\n" ID.pretty isBeforeZero ID.pretty isBeforeEnd;
490-
(`Lifted isBeforeZero,`Lifted isBeforeEnd)
491-
| _ -> (ValueDomainQueries.ID.top (), ValueDomainQueries.ID.top())
492-
end
460+
| _ -> ID.top_of (Cilfacade.ptrdiff_ikind ())
461+
end
462+
| _ ->failwith "unexpected expression in query AllocMayBeOutOfBounds \n"
463+
in
464+
if M.tracing then M.trace "OOB" "e=%a expOffset %a \n" d_exp e ID.pretty expOffset;
465+
let isBeforeZero = ID.le (ID.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero) expOffset in (*check for negative Indices*)
466+
467+
let currentTypSize = size_of_type_in_bytes t in
468+
let castedCurrentTypSize = ID.cast_to (Cilfacade.ptrdiff_ikind ()) currentTypSize in (*add size of type*)
469+
let expOffset_CurrentTyPSize =
470+
begin try ID.add expOffset castedCurrentTypSize
471+
with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of (Cilfacade.ptrdiff_ikind ())
472+
end
473+
in
474+
if M.tracing then M.trace "OOB" "current_index_size %a \n" ID.pretty currentTypSize;
475+
if M.tracing then M.trace "OOB" "expOffset_plus_current_index_size %a \n" ID.pretty expOffset_CurrentTyPSize;
476+
let expOffset_CurrentTypSize_StructOffset =
477+
(try (ID.add o expOffset_CurrentTyPSize)
478+
with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of (Cilfacade.ptrdiff_ikind ()))
479+
in
480+
if M.tracing then M.trace "OOB" "exp_Offset_plus_current_index_size_struct_offset %a \n" ID.pretty expOffset_CurrentTypSize_StructOffset;
481+
let isBeforeEnd = match get_size_of_ptr_target ctx e with
482+
| `Lifted size ->
483+
let casted_e_size = ID.cast_to (Cilfacade.ptrdiff_ikind ()) size in
484+
if M.tracing then M.trace "OOB" "casted_e_size %a \n" ID.pretty casted_e_size;
485+
ID.le expOffset_CurrentTypSize_StructOffset casted_e_size
486+
| `Top -> ID.top_of IInt
487+
| `Bot -> ID.top_of IInt (*Ikind of ID comparisons*)
488+
in
489+
if M.tracing then M.trace "OOB" "result %a %a\n" ID.pretty isBeforeZero ID.pretty isBeforeEnd;
490+
(`Lifted isBeforeZero,`Lifted isBeforeEnd)
491+
| _ -> (ValueDomainQueries.ID.top (), ValueDomainQueries.ID.top())
492+
end
493493
(* Queries.Result.top q *)
494494
| _ -> Queries.Result.top q
495495

‎src/domains/queries.ml‎

Lines changed: 11 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,8 @@ type invariant_context = Invariant.context = {
6262
lvals: Lval.Set.t;
6363
}
6464
[@@deriving ord, hash]
65-
65+
type maybeoutofbounds = {var: CilType.Varinfo.t; dimension: int; index: CilType.Exp.t} [@@deriving ord, hash]
66+
type allocmaybeoutofbounds = {exp: CilType.Exp.t; e1_offset: IntDomain.IntDomTuple.t; struct_offset: IntDomain.IntDomTuple.t; offset_typ: CilType.Typ.t} [@@deriving ord, hash]
6667

6768
(** GADT for queries with specific result type. *)
6869
type _ t =
@@ -126,9 +127,9 @@ type _ t =
126127
| MustTermAllLoops: MustBool.t t
127128
| IsEverMultiThreaded: MayBool.t t
128129
| TmpSpecial: Mval.Exp.t -> ML.t t
129-
| MayBeOutOfBounds: varinfo * int * exp -> ID.t t
130+
| MayBeOutOfBounds: maybeoutofbounds -> ID.t t
130131
| MayOverflow : exp -> MayBool.t t
131-
| AllocMayBeOutOfBounds : exp * IntDomain.IntDomTuple.t * IntDomain.IntDomTuple.t * typ -> VDQ.ProdID.t t
132+
| AllocMayBeOutOfBounds : allocmaybeoutofbounds -> VDQ.ProdID.t t
132133

133134
type 'a result = 'a
134135

@@ -393,31 +394,10 @@ struct
393394
| Any (MayBeModifiedSinceSetjmp e1), Any (MayBeModifiedSinceSetjmp e2) -> JmpBufDomain.BufferEntry.compare e1 e2
394395
| Any (MustBeSingleThreaded {since_start=s1;}), Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2
395396
| Any (TmpSpecial lv1), Any (TmpSpecial lv2) -> Mval.Exp.compare lv1 lv2
396-
| Any (MayBeOutOfBounds (v1, s1, exp1)), Any (MayBeOutOfBounds (v2, s2 ,exp2)) ->
397-
let r = CilType.Varinfo.compare v1 v2 in
398-
if r <> 0 then
399-
r
400-
else if s1 <> s2 then
401-
s1 - s2
402-
else
403-
CilType.Exp.compare exp1 exp2
397+
| Any (MayBeOutOfBounds x1), Any (MayBeOutOfBounds x2) -> compare_maybeoutofbounds x1 x2
404398
(* only argumentless queries should remain *)
405399
| Any (MayOverflow e1), Any (MayOverflow e2) -> CilType.Exp.compare e1 e2
406-
| Any (AllocMayBeOutOfBounds (e1, i1, o1, t1)), Any (AllocMayBeOutOfBounds (e2, i2, o2, t2)) ->
407-
let r = CilType.Exp.compare e1 e2 in
408-
if r <> 0 then
409-
r
410-
else
411-
let r2 = IntDomain.IntDomTuple.compare i1 i2 in
412-
if r2 <> 0 then
413-
r2
414-
else
415-
let r3= IntDomain.IntDomTuple.compare o1 o2 in
416-
if r3 <> 0 then
417-
r3
418-
else
419-
CilType.Typ.compare t1 t2
420-
400+
| Any (AllocMayBeOutOfBounds x1), Any (AllocMayBeOutOfBounds x2) -> compare_allocmaybeoutofbounds x1 x2
421401
| _, _ -> Stdlib.compare (order a) (order b)
422402

423403
let equal x y = compare x y = 0
@@ -458,9 +438,9 @@ struct
458438
| Any (MayBeModifiedSinceSetjmp e) -> JmpBufDomain.BufferEntry.hash e
459439
| Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start
460440
| Any (TmpSpecial lv) -> Mval.Exp.hash lv
461-
| Any (MayBeOutOfBounds (v,s, exp)) -> 67 * CilType.Varinfo.hash v + 31 * Hashtbl.hash s + CilType.Exp.hash exp
441+
| Any (MayBeOutOfBounds x) -> hash_maybeoutofbounds x
462442
| Any (MayOverflow e) -> CilType.Exp.hash e
463-
| Any (AllocMayBeOutOfBounds (e, i, o, t )) -> 127 * CilType.Exp.hash e + 67 * IntDomain.IntDomTuple.hash i + 31 * IntDomain.IntDomTuple.hash o + CilType.Typ.hash t
443+
| Any (AllocMayBeOutOfBounds x) -> hash_allocmaybeoutofbounds x
464444
(* only argumentless queries should remain *)
465445

466446
(* IterSysVars: *)
@@ -525,16 +505,16 @@ struct
525505
| Any MustTermAllLoops -> Pretty.dprintf "MustTermAllLoops"
526506
| Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded"
527507
| Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv
528-
| Any (MayBeOutOfBounds (v,s, e)) -> Pretty.dprintf "MayBeOutOfBounds (%a, %a)" CilType.Varinfo.pretty v CilType.Exp.pretty e
508+
| Any (MayBeOutOfBounds x) -> Pretty.dprintf "MayBeOutOfBounds _"
529509
| Any (MayOverflow e) -> Pretty.dprintf "MayOverflow %a" CilType.Exp.pretty e
530-
| Any (AllocMayBeOutOfBounds (e, i, o, t)) -> Pretty.dprintf "AllocMayBeOutOfBounds _"
510+
| Any (AllocMayBeOutOfBounds x) -> Pretty.dprintf "AllocMayBeOutOfBounds _"
531511
end
532512

533513
let to_value_domain_ask (ask: ask) =
534514
let eval_int e = ask.f (EvalInt e) in
535515
let may_point_to e = ask.f (MayPointTo e) in
536516
let is_multiple v = ask.f (IsMultiple v) in
537-
let may_be_out_of_bounds (v,s) e = ask.f (MayBeOutOfBounds (v, s, e)) in
517+
let may_be_out_of_bounds (v, d) e = ask.f (MayBeOutOfBounds {var= v; dimension= d; index= e}) in
538518
{ VDQ.eval_int; may_point_to; is_multiple; may_be_out_of_bounds}
539519

540520
let eval_int_binop (module Bool: Lattice.S with type t = bool) binop (ask: ask) e1 e2: Bool.t =

0 commit comments

Comments
 (0)