From ddb4f01f9b73fdd56c3938108d58dbf6838af037 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 11 Mar 2020 17:43:44 +0100
Subject: [PATCH] [kernel] Fix Alarms for downcasts on unsigned expressions
---
.Makefile.lint | 2 -
src/kernel_services/ast_data/alarms.ml | 570 ++++++++++++------------
src/kernel_services/ast_data/alarms.mli | 42 +-
tests/rte/oracle/downcast.0.res.oracle | 2 +-
tests/rte/oracle/downcast.2.res.oracle | 4 +-
tests/rte/oracle/minus.0.res.oracle | 2 +-
tests/rte/oracle/minus.1.res.oracle | 8 +-
tests/rte/oracle/mul.res.oracle | 3 +-
tests/value/oracle/downcast.res.oracle | 8 +-
9 files changed, 328 insertions(+), 313 deletions(-)
diff --git a/.Makefile.lint b/.Makefile.lint
index b48bf3c53ff..ab56229610d 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -68,8 +68,6 @@ ML_LINT_KO+=src/kernel_services/analysis/stmts_graph.mli
ML_LINT_KO+=src/kernel_services/analysis/undefined_sequence.ml
ML_LINT_KO+=src/kernel_services/analysis/wto_statement.ml
ML_LINT_KO+=src/kernel_services/analysis/wto_statement.mli
-ML_LINT_KO+=src/kernel_services/ast_data/alarms.ml
-ML_LINT_KO+=src/kernel_services/ast_data/alarms.mli
ML_LINT_KO+=src/kernel_services/ast_data/annotations.ml
ML_LINT_KO+=src/kernel_services/ast_data/annotations.mli
ML_LINT_KO+=src/kernel_services/ast_data/ast.ml
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index eaa9455b742..261c438947f 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -37,22 +37,22 @@ type alarm =
| Division_by_zero of exp
| Memory_access of lval * access_kind
| Index_out_of_bound of
- exp (* index *)
- * exp option (* None = lower bound is zero; Some up = upper bound *)
+ exp (* index *)
+ * exp option (* None = lower bound is zero; Some up = upper bound *)
| Invalid_shift of exp * int option (* strict upper bound, if any *)
| Pointer_comparison of
- exp option (* [None] when implicit comparison to 0 *)
- * exp
+ exp option (* [None] when implicit comparison to 0 *)
+ * exp
| Differing_blocks of exp * exp
| Overflow of
overflow_kind
- * exp
- * Integer.t (* the bound *)
- * bound_kind
+ * exp
+ * Integer.t (* the bound *)
+ * bound_kind
| Float_to_int of
exp
- * Integer.t (* the bound *)
- * bound_kind
+ * Integer.t (* the bound *)
+ * bound_kind
| Not_separated of lval * lval
| Overlap of lval * lval
| Uninitialized of lval
@@ -174,26 +174,26 @@ module D =
else Lval.compare lv1 lv2
) 0 llv1 llv2
| _ -> assert false
- end
- | Dangling lv1, Dangling lv2 -> Lval.compare lv1 lv2
- | Differing_blocks (e11, e12), Differing_blocks (e21, e22) ->
- let n = Exp.compare e11 e21 in
- if n = 0 then Exp.compare e12 e22 else n
- | Function_pointer (e1, l1), Function_pointer (e2, l2) ->
- let n = Exp.compare e1 e2 in
- if n <> 0 then n
- else Extlib.opt_compare (Extlib.list_compare Exp.compare) l1 l2
- | Invalid_bool lv1, Invalid_bool lv2 -> Lval.compare lv1 lv2
- | _, (Division_by_zero _ | Memory_access _ |
- Index_out_of_bound _ | Invalid_shift _ | Pointer_comparison _ |
- Overflow _ | Not_separated _ | Overlap _ | Uninitialized _ |
- Dangling _ | Is_nan_or_infinite _ | Is_nan _ | Float_to_int _ |
- Differing_blocks _ | Function_pointer _ |
- Uninitialized_union _ | Invalid_bool _)
- ->
- let n = nb a1 - nb a2 in
- assert (n <> 0);
- n
+ end
+ | Dangling lv1, Dangling lv2 -> Lval.compare lv1 lv2
+ | Differing_blocks (e11, e12), Differing_blocks (e21, e22) ->
+ let n = Exp.compare e11 e21 in
+ if n = 0 then Exp.compare e12 e22 else n
+ | Function_pointer (e1, l1), Function_pointer (e2, l2) ->
+ let n = Exp.compare e1 e2 in
+ if n <> 0 then n
+ else Extlib.opt_compare (Extlib.list_compare Exp.compare) l1 l2
+ | Invalid_bool lv1, Invalid_bool lv2 -> Lval.compare lv1 lv2
+ | _, (Division_by_zero _ | Memory_access _ |
+ Index_out_of_bound _ | Invalid_shift _ | Pointer_comparison _ |
+ Overflow _ | Not_separated _ | Overlap _ | Uninitialized _ |
+ Dangling _ | Is_nan_or_infinite _ | Is_nan _ | Float_to_int _ |
+ Differing_blocks _ | Function_pointer _ |
+ Uninitialized_union _ | Invalid_bool _)
+ ->
+ let n = nb a1 - nb a2 in
+ assert (n <> 0);
+ n
let equal = Datatype.from_compare
@@ -204,24 +204,24 @@ module D =
| Is_nan (e, fk) ->
Hashtbl.hash (nb a, Exp.hash e, fk)
| Memory_access(lv, b) -> Hashtbl.hash (nb a, Lval.hash lv, b)
- | Index_out_of_bound(e1, e2) ->
+ | Index_out_of_bound(e1, e2) ->
Hashtbl.hash
- (nb a,
- Exp.hash e1,
+ (nb a,
+ Exp.hash e1,
match e2 with None -> 0 | Some e -> 17 + Exp.hash e)
| Invalid_shift(e, n) -> Hashtbl.hash (nb a, Exp.hash e, n)
- | Pointer_comparison(e1, e2) ->
- Hashtbl.hash
- (nb a,
- (match e1 with None -> 0 | Some e -> 17 + Exp.hash e),
+ | Pointer_comparison(e1, e2) ->
+ Hashtbl.hash
+ (nb a,
+ (match e1 with None -> 0 | Some e -> 17 + Exp.hash e),
Exp.hash e2)
- | Differing_blocks (e1, e2) ->
+ | Differing_blocks (e1, e2) ->
Hashtbl.hash (nb a, Exp.hash e1, Exp.hash e2)
| Overflow(s, e, n, b) ->
Hashtbl.hash (s, nb a, Exp.hash e, Integer.hash n, b)
| Float_to_int(e, n, b) ->
Hashtbl.hash (nb a, Exp.hash e, Integer.hash n, b)
- | Not_separated(lv1, lv2) | Overlap(lv1, lv2) ->
+ | Not_separated(lv1, lv2) | Overlap(lv1, lv2) ->
Hashtbl.hash (nb a, Lval.hash lv1, Lval.hash lv2)
| Uninitialized lv -> Hashtbl.hash (nb a, Lval.hash lv)
| Dangling lv -> Hashtbl.hash (nb a, Lval.hash lv)
@@ -235,7 +235,7 @@ module D =
let varname = Datatype.undefined
let pretty fmt = function
- | Division_by_zero e ->
+ | Division_by_zero e ->
Format.fprintf fmt "Division_by_zero(@[%a@])" Printer.pp_exp e
| Is_nan_or_infinite (e, fk) ->
Format.fprintf fmt "Is_nan_or_infinite(@[(%a)%a@])"
@@ -244,14 +244,14 @@ module D =
Format.fprintf fmt "Is_nan(@[(%a)%a@])"
Printer.pp_fkind fk Printer.pp_exp e
| Memory_access(lv, read) ->
- Format.fprintf fmt "Memory_access(@[%a@],@ %s)"
+ Format.fprintf fmt "Memory_access(@[%a@],@ %s)"
Printer.pp_lval lv
(match read with For_reading -> "read" | For_writing -> "write")
| Index_out_of_bound(e1, e2) ->
- Format.fprintf fmt "Index_out_of_bound(@[%a@]@ %s@ @[%a@])"
+ Format.fprintf fmt "Index_out_of_bound(@[%a@]@ %s@ @[%a@])"
Printer.pp_exp e1
(match e2 with None -> ">=" | Some _ -> "<")
- Printer.pp_exp
+ Printer.pp_exp
(match e2 with None -> Cil.zero e1.eloc | Some e -> e)
| Invalid_shift(e, n) ->
Format.fprintf fmt "Invalid_shift(@[%a@]@ %s)"
@@ -259,12 +259,12 @@ module D =
(match n with None -> "" | Some n -> "<= " ^ string_of_int n)
| Pointer_comparison(e1, e2) ->
Format.fprintf fmt "Pointer_comparison(@[%a@],@ @[%a@])"
- Printer.pp_exp
+ Printer.pp_exp
(match e1 with None -> Cil.zero e2.eloc | Some e -> e)
Printer.pp_exp e2
| Differing_blocks (e1, e2) ->
Format.fprintf fmt "Differing_blocks(@[%a@],@ @[%a@])"
- Printer.pp_exp e1 Printer.pp_exp e2
+ Printer.pp_exp e1 Printer.pp_exp e2
| Overflow(s, e, n, b) ->
Format.fprintf fmt "%s(@[%a@]@ %s@ @[%a@])"
(String.capitalize_ascii (string_of_overflow_kind s))
@@ -277,8 +277,8 @@ module D =
(match b with Lower_bound -> ">" | Upper_bound -> "<")
Datatype.Integer.pretty
((match b with
- | Lower_bound -> Integer.sub
- | Upper_bound -> Integer.add) n Integer.one)
+ | Lower_bound -> Integer.sub
+ | Upper_bound -> Integer.add) n Integer.one)
| Not_separated(lv1, lv2) ->
Format.fprintf fmt "Not_separated(@[%a@],@ @[%a@])"
Lval.pretty lv1 Lval.pretty lv2
@@ -292,8 +292,8 @@ module D =
| Function_pointer (e, _) ->
Format.fprintf fmt "Function_pointer(@[%a@])" Exp.pretty e
| Uninitialized_union llv ->
- Format.fprintf fmt "Uninitialized_union(@[[%a]@])"
- (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "; ") Lval.pretty)
+ Format.fprintf fmt "Uninitialized_union(@[[%a]@])"
+ (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "; ") Lval.pretty)
llv
| Invalid_bool lv ->
Format.fprintf fmt "Invalid_bool(@[%a@])" Lval.pretty lv
@@ -301,7 +301,7 @@ module D =
let internal_pretty_code = Datatype.undefined
let copy = Datatype.undefined
let mem_project = Datatype.never_any_project
- end)
+ end)
include D
@@ -320,12 +320,12 @@ module State =
(D.Hashtbl.Make
(Datatype.Quadruple
(Code_annotation)(Kernel_function)(Stmt)(Datatype.Int)))
- (struct
- let name = "Alarms.State"
- let dependencies = [ Ast.self; Rank.self ]
+ (struct
+ let name = "Alarms.State"
+ let dependencies = [ Ast.self; Rank.self ]
let kinds = [ Emitter.Alarm ]
let size = 97
- end)
+ end)
let () =
State.add_hook_on_remove
@@ -344,12 +344,12 @@ module Alarm_of_annot =
let name = "Alarms.Alarm_of_annot"
let dependencies = [ Ast.self; Rank.self ]
let size = 97
- end)
+ end)
let self = State.self
let () = Ast.add_monotonic_state self
-let emit_status emitter kf stmt annot status =
+let emit_status emitter kf stmt annot status =
let p = Property.ip_of_code_annot_single kf stmt annot in
Property_status.emit emitter ~hyps:[] p ~distinct:true status
@@ -360,17 +360,17 @@ let emit_status emitter kf stmt annot status =
let alarm_kf_stmt ?kf kinstr =
match kinstr with
| Kglobal -> begin
- let kf = match kf with
- | None -> fst (Globals.entry_point ())
- | Some kf ->
- Kernel.fatal "inconsistency in alarm location" Kernel_function.pretty kf
- in
- try
- let stmt = Kernel_function.find_first_stmt kf in
- kf, stmt
- with Kernel_function.No_Statement ->
- (* TODO: this can actually happen *)
- Kernel.fatal "[Alarm] main function has no code"
+ let kf = match kf with
+ | None -> fst (Globals.entry_point ())
+ | Some kf ->
+ Kernel.fatal "inconsistency in alarm location" Kernel_function.pretty kf
+ in
+ try
+ let stmt = Kernel_function.find_first_stmt kf in
+ kf, stmt
+ with Kernel_function.No_Statement ->
+ (* TODO: this can actually happen *)
+ Kernel.fatal "[Alarm] main function has no code"
end
| Kstmt stmt -> begin
let kf = match kf with
@@ -433,24 +433,24 @@ let get_description = function
(* Given a "topmost" location and another one supposed to be more precise,
returns the best (hopefully not unknown) one. *)
let best_loc ~loc loc' =
- if Location.equal loc' Location.unknown then loc else loc'
+ if Location.equal loc' Location.unknown then loc else loc'
let overflowed_expr_to_term ~loc e =
let loc = best_loc ~loc e.eloc in
match e.enode with
- | UnOp(op, e, ty) ->
+ | UnOp(op, e, ty) ->
let t = Logic_utils.expr_to_term ~cast:true e in
let ty = Logic_utils.typ_to_logic_type ty in
Logic_const.term ~loc (TUnOp(op, t)) ty
- | BinOp(op, e1, e2, ty) ->
+ | BinOp(op, e1, e2, ty) ->
let t1 = Logic_utils.expr_to_term ~cast:true e1 in
let t2 = Logic_utils.expr_to_term ~cast:true e2 in
let ty = Logic_utils.typ_to_logic_type ty in
Logic_const.term ~loc (TBinOp(op, t1, t2)) ty
| _ -> Logic_utils.expr_to_term ~cast:true e
- (* Creates \is_finite((fkind)e) or \is_nan((fkind)e) according to
- [predicate]. *)
+(* Creates \is_finite((fkind)e) or \is_nan((fkind)e) according to
+ [predicate]. *)
let create_special_float_predicate ~loc e fkind predicate =
let loc = best_loc ~loc e.eloc in
let t = Logic_utils.expr_to_term ~cast:true e in
@@ -473,174 +473,188 @@ let create_special_float_predicate ~loc e fkind predicate =
in
Logic_const.unamed ~loc (Papp (pi, [], [ t ]))
-let create_predicate ?(loc=Location.unknown) alarm =
+let create_predicate ?(loc=Location.unknown) alarm =
let aux = function
- | Division_by_zero e ->
- (* e != 0 *)
- let loc = best_loc ~loc e.eloc in
- let t = Logic_utils.expr_to_term ~cast:true e in
- Logic_const.prel ~loc (Rneq, t, Cil.lzero ())
-
- | Memory_access(lv, read) ->
- (* \valid(lv) or \valid_read(lv) according to read *)
- let valid = match read with
- | For_reading -> Logic_const.pvalid_read
- | For_writing -> Logic_const.pvalid
- in
- let e = Cil.mkAddrOrStartOf ~loc lv in
- let t = Logic_utils.expr_to_term ~cast:true e in
- valid ~loc (Logic_const.here_label, t)
-
- | Index_out_of_bound(e1, e2) ->
- (* 0 <= e1 < e2, left part if None, right part if Some e *)
- let loc = best_loc ~loc e1.eloc in
- let t1 = Logic_utils.expr_to_term ~cast:true e1 in
- (match e2 with
- | None -> Logic_const.prel ~loc (Rle, Cil.lzero (), t1)
- | Some e2 ->
+ | Division_by_zero e ->
+ (* e != 0 *)
+ let loc = best_loc ~loc e.eloc in
+ let t = Logic_utils.expr_to_term ~cast:true e in
+ Logic_const.prel ~loc (Rneq, t, Cil.lzero ())
+
+ | Memory_access(lv, read) ->
+ (* \valid(lv) or \valid_read(lv) according to read *)
+ let valid = match read with
+ | For_reading -> Logic_const.pvalid_read
+ | For_writing -> Logic_const.pvalid
+ in
+ let e = Cil.mkAddrOrStartOf ~loc lv in
+ let t = Logic_utils.expr_to_term ~cast:true e in
+ valid ~loc (Logic_const.here_label, t)
+
+ | Index_out_of_bound(e1, e2) ->
+ (* 0 <= e1 < e2, left part if None, right part if Some e *)
+ let loc = best_loc ~loc e1.eloc in
+ let t1 = Logic_utils.expr_to_term ~cast:true e1 in
+ (match e2 with
+ | None -> Logic_const.prel ~loc (Rle, Cil.lzero (), t1)
+ | Some e2 ->
+ let t2 = Logic_utils.expr_to_term ~cast:true e2 in
+ Logic_const.prel ~loc (Rlt, t1, t2))
+
+ | Invalid_shift(e, n) ->
+ (* 0 <= e < n *)
+ let loc = best_loc ~loc e.eloc in
+ let t = Logic_utils.expr_to_term ~cast:true e in
+ let low_cmp = Logic_const.prel ~loc (Rle, Cil.lzero (), t) in
+ (match n with
+ | None -> low_cmp
+ | Some n ->
+ let tn = Logic_const.tint ~loc (Integer.of_int n) in
+ let up_cmp = Logic_const.prel ~loc (Rlt, t, tn) in
+ Logic_const.pand ~loc (low_cmp, up_cmp))
+
+ | Pointer_comparison(e1, e2) ->
+ (* \pointer_comparable(e1, e2) *)
+ let loc = best_loc ~loc e2.eloc in
+ let t1 = match e1 with
+ | None -> begin
+ let typ = match Cil.unrollTypeDeep (Cil.typeOf e2) with
+ | TPtr (TFun _, _) -> TPtr (TFun(Cil.voidType, None, false, []), [])
+ | _ -> Cil.voidPtrType
+ in
+ let zero = Cil.lzero () in
+ Logic_const.term (TCastE (typ, zero)) (Ctype typ)
+ end
+ | Some e -> Logic_utils.expr_to_term ~cast:true e
+ in
let t2 = Logic_utils.expr_to_term ~cast:true e2 in
- Logic_const.prel ~loc (Rlt, t1, t2))
-
- | Invalid_shift(e, n) ->
- (* 0 <= e < n *)
- let loc = best_loc ~loc e.eloc in
- let t = Logic_utils.expr_to_term ~cast:true e in
- let low_cmp = Logic_const.prel ~loc (Rle, Cil.lzero (), t) in
- (match n with
- | None -> low_cmp
- | Some n ->
- let tn = Logic_const.tint ~loc (Integer.of_int n) in
- let up_cmp = Logic_const.prel ~loc (Rlt, t, tn) in
- Logic_const.pand ~loc (low_cmp, up_cmp))
-
- | Pointer_comparison(e1, e2) ->
- (* \pointer_comparable(e1, e2) *)
- let loc = best_loc ~loc e2.eloc in
- let t1 = match e1 with
- | None -> begin
- let typ = match Cil.unrollTypeDeep (Cil.typeOf e2) with
- | TPtr (TFun _, _) -> TPtr (TFun(Cil.voidType, None, false, []), [])
- | _ -> Cil.voidPtrType
- in
- let zero = Cil.lzero () in
- Logic_const.term (TCastE (typ, zero)) (Ctype typ)
- end
- | Some e -> Logic_utils.expr_to_term ~cast:true e
- in
- let t2 = Logic_utils.expr_to_term ~cast:true e2 in
- Logic_utils.pointer_comparable ~loc t1 t2
-
- | Differing_blocks(e1, e2) ->
- (* \base_addr(e1) == \base_addr(e2) *)
- let loc = best_loc ~loc e1.eloc in
- let t1 = Logic_utils.expr_to_term ~cast:true e1 in
- let here = Logic_const.here_label in
- let typ = Ctype Cil.charPtrType in
- let t1 =
- Logic_const.term ~loc:(best_loc loc e1.eloc) (Tbase_addr(here, t1)) typ
- in
- let t2 = Logic_utils.expr_to_term ~cast:true e2 in
- let t2 =
- Logic_const.term ~loc:(best_loc loc e2.eloc) (Tbase_addr(here, t2)) typ
- in
- Logic_const.prel ~loc (Req, t1, t2)
-
- | Overflow(_, e, n, bound) ->
- (* n <= e or e <= n according to bound *)
- let loc = best_loc ~loc e.eloc in
- let t = overflowed_expr_to_term ~loc e in
- let tn = Logic_const.tint ~loc n in
- Logic_const.prel ~loc
- (match bound with Lower_bound -> Rle, tn, t | Upper_bound -> Rle, t, tn)
-
- | Float_to_int(e, n, bound) ->
- (* n < e or e < n according to bound *)
- let loc = best_loc ~loc e.eloc in
- let te = overflowed_expr_to_term ~loc e in
- let t = Logic_const.tlogic_coerce ~loc te Lreal in
- let n =
- (match bound with Lower_bound -> Integer.sub | Upper_bound -> Integer.add)
- n Integer.one
- in
- let tn = Logic_const.tlogic_coerce ~loc (Logic_const.tint ~loc n) Lreal in
- Logic_const.prel ~loc
- (match bound with Lower_bound -> Rlt, tn, t | Upper_bound -> Rlt, t, tn)
-
- | Not_separated(lv1, lv2) ->
- (* \separated(lv1, lv2) *)
- let e1 = Cil.mkAddrOf ~loc lv1 in
- let t1 = Logic_utils.expr_to_term ~cast:true e1 in
- let e2 = Cil.mkAddrOf ~loc lv2 in
- let t2 = Logic_utils.expr_to_term ~cast:true e2 in
- Logic_const.pseparated ~loc [ t1; t2 ]
+ Logic_utils.pointer_comparable ~loc t1 t2
+
+ | Differing_blocks(e1, e2) ->
+ (* \base_addr(e1) == \base_addr(e2) *)
+ let loc = best_loc ~loc e1.eloc in
+ let t1 = Logic_utils.expr_to_term ~cast:true e1 in
+ let here = Logic_const.here_label in
+ let typ = Ctype Cil.charPtrType in
+ let t1 =
+ Logic_const.term ~loc:(best_loc loc e1.eloc) (Tbase_addr(here, t1)) typ
+ in
+ let t2 = Logic_utils.expr_to_term ~cast:true e2 in
+ let t2 =
+ Logic_const.term ~loc:(best_loc loc e2.eloc) (Tbase_addr(here, t2)) typ
+ in
+ Logic_const.prel ~loc (Req, t1, t2)
+
+ | Overflow(kind, e, n, bound) ->
+ (* n <= e or e <= n according to bound *)
+ let loc = best_loc ~loc e.eloc in
+ let exp_type = Cil.typeOf e in
+ let t = match kind with
+ | Signed_downcast | Unsigned_downcast
+ when Cil.isUnsignedInteger exp_type ->
+ let t = overflowed_expr_to_term ~loc e in
+ (* Without this cast, the alarm is:
+ - Signed_downcast: unsound ->
+ uint x=0; int i=(x-1u); // 0u-1u < INT_MAX: OK
+ - Unsigned_downcast: too restrictive ->
+ uint x=UINT_MAX; uchar i=(x+1u); // UINT_MAX+1 < UCHAR_MAX : NOK
+ *)
+ Logic_utils.mk_cast exp_type t
+ | _ ->
+ overflowed_expr_to_term ~loc e
+ in
+ let tn = Logic_const.tint ~loc n in
+ Logic_const.prel ~loc
+ (match bound with Lower_bound -> Rle, tn, t | Upper_bound -> Rle, t, tn)
+
+ | Float_to_int(e, n, bound) ->
+ (* n < e or e < n according to bound *)
+ let loc = best_loc ~loc e.eloc in
+ let te = overflowed_expr_to_term ~loc e in
+ let t = Logic_const.tlogic_coerce ~loc te Lreal in
+ let n =
+ (match bound with Lower_bound -> Integer.sub | Upper_bound -> Integer.add)
+ n Integer.one
+ in
+ let tn = Logic_const.tlogic_coerce ~loc (Logic_const.tint ~loc n) Lreal in
+ Logic_const.prel ~loc
+ (match bound with Lower_bound -> Rlt, tn, t | Upper_bound -> Rlt, t, tn)
+
+ | Not_separated(lv1, lv2) ->
+ (* \separated(lv1, lv2) *)
+ let e1 = Cil.mkAddrOf ~loc lv1 in
+ let t1 = Logic_utils.expr_to_term ~cast:true e1 in
+ let e2 = Cil.mkAddrOf ~loc lv2 in
+ let t2 = Logic_utils.expr_to_term ~cast:true e2 in
+ Logic_const.pseparated ~loc [ t1; t2 ]
- | Overlap(lv1, lv2) ->
- (* (lv1 == lv2) || \separated(lv1, lv2) *)
- let e1 = Cil.mkAddrOf ~loc lv1 in
- let t1 = Logic_utils.expr_to_term ~cast:true e1 in
- let e2 = Cil.mkAddrOf ~loc lv2 in
- let t2 = Logic_utils.expr_to_term ~cast:true e2 in
- let eq = Logic_const.prel ~loc (Req, t1, t2) in
- let sep = Logic_const.pseparated ~loc [ t1; t2 ] in
- Logic_const.por ~loc (eq, sep)
-
- | Uninitialized lv ->
- (* \initialized(lv) *)
- let e = Cil.mkAddrOrStartOf ~loc lv in
- let t = Logic_utils.expr_to_term ~cast:false e in
- Logic_const.pinitialized ~loc (Logic_const.here_label, t)
-
- | Dangling lv ->
- (* !\dangling(lv) *)
- let e = Cil.mkAddrOrStartOf ~loc lv in
- let t = Logic_utils.expr_to_term ~cast:false e in
- Logic_const.(pnot ~loc (pdangling ~loc (Logic_const.here_label, t)))
-
- | Is_nan_or_infinite (e, fkind) ->
- create_special_float_predicate ~loc e fkind "\\is_finite"
- | Is_nan (e, fkind) ->
- let pred = create_special_float_predicate ~loc e fkind "\\is_NaN" in
- Logic_const.pnot ~loc pred
-
- | Function_pointer (e, args) ->
- let loc = e.eloc in
- let t = Cil.typeOf e in
- let e =
- match Cil.unrollTypeDeep t, args with
- | TPtr (TFun (_, Some _, _, _), _), _
- | TPtr (TFun _, _), None -> e
- | TPtr (TFun (ret, None, var, attrs), _), Some args ->
- let ltyps = List.map (fun arg -> "", Cil.typeOf arg, []) args in
- let typ = TFun (ret, Some ltyps, var, attrs) in
- Cil.mkCast e (TPtr (typ, []))
- | t', _ ->
- Kernel.fatal
- "Trying to emit a Function_pointer alarm over expression %a \
- that has unexpected type %a (unrolled as %a)"
- Printer.pp_exp e Printer.pp_typ t Printer.pp_typ t'
- in
- let t = Logic_utils.expr_to_term ~cast:true e in
- Logic_const.(pvalid_function ~loc t)
+ | Overlap(lv1, lv2) ->
+ (* (lv1 == lv2) || \separated(lv1, lv2) *)
+ let e1 = Cil.mkAddrOf ~loc lv1 in
+ let t1 = Logic_utils.expr_to_term ~cast:true e1 in
+ let e2 = Cil.mkAddrOf ~loc lv2 in
+ let t2 = Logic_utils.expr_to_term ~cast:true e2 in
+ let eq = Logic_const.prel ~loc (Req, t1, t2) in
+ let sep = Logic_const.pseparated ~loc [ t1; t2 ] in
+ Logic_const.por ~loc (eq, sep)
- | Uninitialized_union llv ->
- (* \initialized(lv_1) || ... || \initialized(lv_n) *)
- let make_lval_predicate lv =
+ | Uninitialized lv ->
+ (* \initialized(lv) *)
let e = Cil.mkAddrOrStartOf ~loc lv in
let t = Logic_utils.expr_to_term ~cast:false e in
Logic_const.pinitialized ~loc (Logic_const.here_label, t)
- in
- List.fold_left (fun acc lv ->
- Logic_const.por ~loc (acc, make_lval_predicate lv)
- )
- (make_lval_predicate (List.hd llv))
- (List.tl llv)
-
- | Invalid_bool lv ->
- let e = Cil.new_exp ~loc (Lval lv) in
- let t = Logic_utils.expr_to_term ~cast:false e in
- let zero = Logic_const.prel ~loc (Req, t, Cil.lzero ()) in
- let one = Logic_const.prel ~loc (Req, t, Cil.lone ()) in
- Logic_const.por ~loc (zero, one)
+
+ | Dangling lv ->
+ (* !\dangling(lv) *)
+ let e = Cil.mkAddrOrStartOf ~loc lv in
+ let t = Logic_utils.expr_to_term ~cast:false e in
+ Logic_const.(pnot ~loc (pdangling ~loc (Logic_const.here_label, t)))
+
+ | Is_nan_or_infinite (e, fkind) ->
+ create_special_float_predicate ~loc e fkind "\\is_finite"
+ | Is_nan (e, fkind) ->
+ let pred = create_special_float_predicate ~loc e fkind "\\is_NaN" in
+ Logic_const.pnot ~loc pred
+
+ | Function_pointer (e, args) ->
+ let loc = e.eloc in
+ let t = Cil.typeOf e in
+ let e =
+ match Cil.unrollTypeDeep t, args with
+ | TPtr (TFun (_, Some _, _, _), _), _
+ | TPtr (TFun _, _), None -> e
+ | TPtr (TFun (ret, None, var, attrs), _), Some args ->
+ let ltyps = List.map (fun arg -> "", Cil.typeOf arg, []) args in
+ let typ = TFun (ret, Some ltyps, var, attrs) in
+ Cil.mkCast e (TPtr (typ, []))
+ | t', _ ->
+ Kernel.fatal
+ "Trying to emit a Function_pointer alarm over expression %a \
+ that has unexpected type %a (unrolled as %a)"
+ Printer.pp_exp e Printer.pp_typ t Printer.pp_typ t'
+ in
+ let t = Logic_utils.expr_to_term ~cast:true e in
+ Logic_const.(pvalid_function ~loc t)
+
+ | Uninitialized_union llv ->
+ (* \initialized(lv_1) || ... || \initialized(lv_n) *)
+ let make_lval_predicate lv =
+ let e = Cil.mkAddrOrStartOf ~loc lv in
+ let t = Logic_utils.expr_to_term ~cast:false e in
+ Logic_const.pinitialized ~loc (Logic_const.here_label, t)
+ in
+ List.fold_left (fun acc lv ->
+ Logic_const.por ~loc (acc, make_lval_predicate lv)
+ )
+ (make_lval_predicate (List.hd llv))
+ (List.tl llv)
+
+ | Invalid_bool lv ->
+ let e = Cil.new_exp ~loc (Lval lv) in
+ let t = Logic_utils.expr_to_term ~cast:false e in
+ let zero = Logic_const.prel ~loc (Req, t, Cil.lzero ()) in
+ let one = Logic_const.prel ~loc (Req, t, Cil.lone ()) in
+ Logic_const.por ~loc (zero, one)
in
let p = aux alarm in
assert (p.pred_name = []);
@@ -651,11 +665,11 @@ let find_alarm_in_emitters tbl alarm =
try
Usable_emitter.Hashtbl.iter
(fun _ h ->
- try
- let triple = D.Hashtbl.find h alarm in
- raise (Found triple)
- with Not_found ->
- ())
+ try
+ let triple = D.Hashtbl.find h alarm in
+ raise (Found triple)
+ with Not_found ->
+ ())
tbl;
None
with Found x ->
@@ -666,7 +680,7 @@ let find_alarm_in_emitters tbl alarm =
whether said code annotation is new, and the table in which the code annot
is/should be inserted. *)
let to_annot_aux kinstr ?(loc=Kinstr.loc kinstr) alarm =
-(* Kernel.debug "registering alarm %a" D.pretty alarm;*)
+ (* Kernel.debug "registering alarm %a" D.pretty alarm;*)
let add alarm =
let pred = create_predicate ~loc alarm in
Logic_const.new_code_annotation (AAssert([], Assert, pred))
@@ -715,48 +729,48 @@ let register emitter ?kf kinstr ?loc ?status alarm =
let iter f =
State.iter
(fun _ by_emitter ->
- Usable_emitter.Hashtbl.iter
- (fun e h ->
- D.Hashtbl.iter
- (fun alarm (annot, kf, stmt, rank) ->
- f (Usable_emitter.get e) kf stmt ~rank alarm annot)
- h)
- by_emitter)
+ Usable_emitter.Hashtbl.iter
+ (fun e h ->
+ D.Hashtbl.iter
+ (fun alarm (annot, kf, stmt, rank) ->
+ f (Usable_emitter.get e) kf stmt ~rank alarm annot)
+ h)
+ by_emitter)
let fold f =
State.fold
(fun _ by_emitter acc ->
- Usable_emitter.Hashtbl.fold
- (fun e h acc ->
- D.Hashtbl.fold
- (fun alarm (annot, kf, stmt, rank) acc ->
- f (Usable_emitter.get e) kf stmt ~rank alarm annot acc)
- h
- acc)
- by_emitter
- acc)
-
-let find annot =
+ Usable_emitter.Hashtbl.fold
+ (fun e h acc ->
+ D.Hashtbl.fold
+ (fun alarm (annot, kf, stmt, rank) acc ->
+ f (Usable_emitter.get e) kf stmt ~rank alarm annot acc)
+ h
+ acc)
+ by_emitter
+ acc)
+
+let find annot =
try Some (Alarm_of_annot.find annot)
with Not_found -> None
-let unsafe_remove ?filter ?kinstr e =
+let unsafe_remove ?filter ?kinstr e =
let usable_e = Emitter.get e in
- let remove also_alarm by_emitter =
+ let remove also_alarm by_emitter =
try
let tbl = Usable_emitter.Hashtbl.find by_emitter usable_e in
let to_be_removed = D.Hashtbl.create 7 in
let stmt_ref = ref Cil.dummyStmt in
- let extend_del a (annot, _, stmt, _ as t) =
+ let extend_del a (annot, _, stmt, _ as t) =
D.Hashtbl.add to_be_removed a t;
Alarm_of_annot.remove annot;
stmt_ref := stmt
in
D.Hashtbl.iter
- (fun alarm v ->
- match filter with
- | Some f when not (f alarm) -> ()
- | _ -> extend_del alarm v)
+ (fun alarm v ->
+ match filter with
+ | Some f when not (f alarm) -> ()
+ | _ -> extend_del alarm v)
tbl;
if also_alarm then begin
let remove alarm _ = D.Hashtbl.remove tbl alarm in
@@ -765,20 +779,20 @@ let unsafe_remove ?filter ?kinstr e =
[filtered_remove] *)
State.apply_hooks_on_remove
(Emitter.get e)
- (Kstmt !stmt_ref)
+ (Kstmt !stmt_ref)
to_be_removed
with Not_found ->
()
in
- let filtered_remove tbl = match filter with
- | None ->
+ let filtered_remove tbl = match filter with
+ | None ->
remove false tbl;
Usable_emitter.Hashtbl.remove tbl usable_e
- | Some _ ->
+ | Some _ ->
remove true tbl
in
match kinstr with
- | None ->
+ | None ->
State.iter (fun _ by_emitter -> filtered_remove by_emitter)
| Some ki ->
try
@@ -790,18 +804,18 @@ let unsafe_remove ?filter ?kinstr e =
let remove ?filter ?kinstr e =
unsafe_remove ?filter ?kinstr e
-let () =
+let () =
Annotations.remove_alarm_ref :=
(fun e stmt annot ->
- try
- let a = Alarm_of_annot.find annot in
- (* [JS 2013/01/09] could be more efficient but seems we only consider
- the alarms of one statement, it should be enough yet *)
- let filter a' = a == a' in
- let kinstr = Kstmt stmt in
- remove ~filter ~kinstr (Emitter.Usable_emitter.get e)
- with Not_found ->
- ())
+ try
+ let a = Alarm_of_annot.find annot in
+ (* [JS 2013/01/09] could be more efficient but seems we only consider
+ the alarms of one statement, it should be enough yet *)
+ let filter a' = a == a' in
+ let kinstr = Kstmt stmt in
+ remove ~filter ~kinstr (Emitter.Usable_emitter.get e)
+ with Not_found ->
+ ())
(*
Local Variables:
diff --git a/src/kernel_services/ast_data/alarms.mli b/src/kernel_services/ast_data/alarms.mli
index c8a332f79f1..daac448c4ea 100644
--- a/src/kernel_services/ast_data/alarms.mli
+++ b/src/kernel_services/ast_data/alarms.mli
@@ -37,24 +37,24 @@ type alarm =
| Division_by_zero of exp
| Memory_access of lval * access_kind
| Index_out_of_bound of
- exp (** index *)
- * exp option (** None = lower bound is zero; Some up = upper bound *)
+ exp (** index *)
+ * exp option (** None = lower bound is zero; Some up = upper bound *)
| Invalid_shift of exp * int option (** strict upper bound, if any *)
- | Pointer_comparison of
- exp option (** [None] when implicit comparison to NULL pointer *)
- * exp
+ | Pointer_comparison of
+ exp option (** [None] when implicit comparison to NULL pointer *)
+ * exp
| Differing_blocks of exp * exp (** The two expressions (which evaluate to
- pointers) must point to the same allocated block *)
+ pointers) must point to the same allocated block *)
| Overflow of
overflow_kind
- * exp
- * Integer.t (** the bound *)
- * bound_kind
+ * exp
+ * Integer.t (** the bound *)
+ * bound_kind
| Float_to_int of
exp
- * Integer.t (** the bound for the integer type. The actual alarm
- is [exp < bound+1] or [bound-1 < exp]. *)
- * bound_kind
+ * Integer.t (** the bound for the integer type. The actual alarm
+ is [exp < bound+1] or [bound-1 < exp]. *)
+ * bound_kind
| Not_separated of lval * lval (** the two lvalues must be separated *)
| Overlap of lval * lval (** overlapping read/write: the two lvalues must be
separated or equal *)
@@ -73,8 +73,8 @@ include Datatype.S_with_collections with type t = alarm
val self: State.t
-val register:
- Emitter.t -> ?kf:kernel_function -> kinstr -> ?loc:location ->
+val register:
+ Emitter.t -> ?kf:kernel_function -> kinstr -> ?loc:location ->
?status:Property_status.emitted_status -> alarm ->
code_annotation * bool
(** Register the given alarm on the given statement. By default, no status is
@@ -82,7 +82,7 @@ val register:
must be the function enclosing this statement.
@return true if the given alarm has never been emitted before on the
same kinstr (without taking into consideration the status or
- the emitter).
+ the emitter).
@modify Oxygen-20120901 remove labeled argument ~deps
@modify Fluorine-20130401 add the optional arguments [kf], [loc] and
@@ -95,18 +95,18 @@ val to_annot: kinstr -> ?loc:location -> alarm -> code_annotation * bool
The returned boolean indicates that the alarm has not been registered
in the kernel yet. *)
-val iter:
+val iter:
(Emitter.t -> kernel_function -> stmt -> rank:int -> alarm -> code_annotation
- -> unit)
+ -> unit)
-> unit
(** Iterator over all alarms and the associated annotations at some program
point.
@since Fluorine-20130401 *)
-val fold:
+val fold:
(Emitter.t -> kernel_function -> stmt -> rank:int -> alarm -> code_annotation
-> 'a
- -> 'a)
+ -> 'a)
-> 'a
-> 'a
(** Folder over all alarms and the associated annotations at some program
@@ -121,11 +121,11 @@ val remove: ?filter:(alarm -> bool) -> ?kinstr:kinstr -> Emitter.t -> unit
(** Remove the alarms and the associated annotations emitted by the given
emitter. If [kinstr] is specified, remove only the ones associated with this
kinstr. If [filter] is specified, remove only the alarms [a] such that
- [filter a] is [true].
+ [filter a] is [true].
@since Fluorine-20130401 *)
val create_predicate: ?loc:location -> t -> predicate
-(** Generate the predicate corresponding to a given alarm.
+(** Generate the predicate corresponding to a given alarm.
@since Fluorine-20130401 *)
val get_name: t -> string
diff --git a/tests/rte/oracle/downcast.0.res.oracle b/tests/rte/oracle/downcast.0.res.oracle
index e5947116b6b..5963c8e9adf 100644
--- a/tests/rte/oracle/downcast.0.res.oracle
+++ b/tests/rte/oracle/downcast.0.res.oracle
@@ -22,7 +22,7 @@ int main(void)
/*@ assert rte: signed_overflow: (int)sx + (int)sy ≤ 2147483647; */
uc = (unsigned char)((int)sx + (int)sy);
uc = (unsigned char)x;
- /*@ assert rte: signed_downcast: uy + uz ≤ 2147483647; */
+ /*@ assert rte: signed_downcast: (unsigned int)(uy + uz) ≤ 2147483647; */
x = (int)(uy + uz);
ux = uy + uz;
s = (unsigned short)(uy + uz);
diff --git a/tests/rte/oracle/downcast.2.res.oracle b/tests/rte/oracle/downcast.2.res.oracle
index c6bce9ea5ca..dd0102f2be0 100644
--- a/tests/rte/oracle/downcast.2.res.oracle
+++ b/tests/rte/oracle/downcast.2.res.oracle
@@ -26,10 +26,10 @@ int main(void)
/*@ assert rte: unsigned_downcast: x ≤ 255; */
/*@ assert rte: unsigned_downcast: 0 ≤ x; */
uc = (unsigned char)x;
- /*@ assert rte: signed_downcast: uy + uz ≤ 2147483647; */
+ /*@ assert rte: signed_downcast: (unsigned int)(uy + uz) ≤ 2147483647; */
x = (int)(uy + uz);
ux = uy + uz;
- /*@ assert rte: unsigned_downcast: uy + uz ≤ 65535; */
+ /*@ assert rte: unsigned_downcast: (unsigned int)(uy + uz) ≤ 65535; */
s = (unsigned short)(uy + uz);
__retres = 0;
return __retres;
diff --git a/tests/rte/oracle/minus.0.res.oracle b/tests/rte/oracle/minus.0.res.oracle
index 2944e5aa989..ea9f8124d52 100644
--- a/tests/rte/oracle/minus.0.res.oracle
+++ b/tests/rte/oracle/minus.0.res.oracle
@@ -28,7 +28,7 @@ int main(void)
z = - x;
/*@ assert rte: signed_overflow: -2147483647 ≤ (int)(-0x7fffffff) - 1; */
z = - (-0x7fffffff - 1);
- /*@ assert rte: signed_downcast: -ux ≤ 2147483647; */
+ /*@ assert rte: signed_downcast: (unsigned int)(-ux) ≤ 2147483647; */
z = (int)(- ux);
/*@ assert
rte: signed_overflow:
diff --git a/tests/rte/oracle/minus.1.res.oracle b/tests/rte/oracle/minus.1.res.oracle
index e3e98049c15..8e295b1e3cf 100644
--- a/tests/rte/oracle/minus.1.res.oracle
+++ b/tests/rte/oracle/minus.1.res.oracle
@@ -20,7 +20,7 @@ int main(void)
/*@ assert rte: signed_overflow: (int)(-0x7fffffff) - 1 ≤ 2147483647; */
/*@ assert rte: signed_overflow: -2147483647 ≤ (int)(-0x7fffffff) - 1; */
z = - (-0x7fffffff - 1);
- /*@ assert rte: signed_downcast: -ux ≤ 2147483647; */
+ /*@ assert rte: signed_downcast: (unsigned int)(-ux) ≤ 2147483647; */
z = (int)(- ux);
/*@ assert rte: signed_overflow: -2147483648 ≤ 65535 + 3; */
/*@ assert rte: signed_overflow: 65535 + 3 ≤ 2147483647; */
@@ -43,12 +43,14 @@ int main(void)
sz = (short)((int)((unsigned short)(65535 + 3)) + x);
/*@ assert
rte: signed_downcast:
- (unsigned int)(-0x80000000) - (unsigned int)1 ≤ 2147483647;
+ (unsigned int)((unsigned int)(-0x80000000) - (unsigned int)1) ≤
+ 2147483647;
*/
z = (int)(-0x80000000 - (unsigned int)1);
/*@ assert
rte: signed_downcast:
- (unsigned int)(-2147483648) - (unsigned int)1 ≤ 2147483647;
+ (unsigned int)((unsigned int)(-2147483648) - (unsigned int)1) ≤
+ 2147483647;
*/
z = (int)(-2147483648 - (unsigned int)1);
/*@ assert rte: signed_overflow: -2147483647 ≤ 2147483647; */
diff --git a/tests/rte/oracle/mul.res.oracle b/tests/rte/oracle/mul.res.oracle
index cde812eaa97..a30e7ac4626 100644
--- a/tests/rte/oracle/mul.res.oracle
+++ b/tests/rte/oracle/mul.res.oracle
@@ -36,7 +36,8 @@ int main(void)
z = x * 1;
z = 1 * y;
/*@ assert
- rte: signed_downcast: (unsigned int)x * 0xffffffff ≤ 2147483647;
+ rte: signed_downcast:
+ (unsigned int)((unsigned int)x * 0xffffffff) ≤ 2147483647;
*/
z = (int)((unsigned int)x * 0xffffffff);
/*@ assert rte: signed_overflow: 0xffff * 0xffff ≤ 2147483647; */
diff --git a/tests/value/oracle/downcast.res.oracle b/tests/value/oracle/downcast.res.oracle
index 2876a38c281..7df2a56ff7b 100644
--- a/tests/value/oracle/downcast.res.oracle
+++ b/tests/value/oracle/downcast.res.oracle
@@ -20,7 +20,7 @@
[eva:alarm] tests/value/downcast.i:19: Warning:
signed downcast. assert (int)sx + (int)sy ≤ 127;
[eva:alarm] tests/value/downcast.i:22: Warning:
- signed downcast. assert uy + uz ≤ 2147483647;
+ signed downcast. assert (unsigned int)(uy + uz) ≤ 2147483647;
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2_bitfield <- main.
@@ -445,7 +445,7 @@ void main1(void)
sz = (signed char)((int)sx + (int)sy);
uc = (unsigned char)((int)sx + (int)sy);
uc = (unsigned char)x;
- /*@ assert Eva: signed_downcast: uy + uz ≤ 2147483647; */
+ /*@ assert Eva: signed_downcast: (unsigned int)(uy + uz) ≤ 2147483647; */
x = (int)(uy + uz);
ux = uy + uz;
s = (unsigned short)(uy + uz);
@@ -648,7 +648,7 @@ void main(void)
[eva:alarm] tests/value/downcast.i:21: Warning:
unsigned downcast. assert x ≤ 255;
[eva:alarm] tests/value/downcast.i:24: Warning:
- unsigned downcast. assert uy + uz ≤ 65535;
+ unsigned downcast. assert (unsigned int)(uy + uz) ≤ 65535;
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2_bitfield <- main.
@@ -1004,7 +1004,7 @@ void main1(void)
uc = (unsigned char)x;
x = (int)(uy + uz);
ux = uy + uz;
- /*@ assert Eva: unsigned_downcast: uy + uz ≤ 65535; */
+ /*@ assert Eva: unsigned_downcast: (unsigned int)(uy + uz) ≤ 65535; */
s = (unsigned short)(uy + uz);
return;
}
--
GitLab