From 2154c2c48332c2ce131b180fa4a34a4cf4922d85 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 13 Jul 2016 15:56:47 -0700 Subject: [PATCH] Refactor Sil.unop into separate Unop module Summary: Move Sil.unop type and operations into separate Unop module. Reviewed By: dulmarod Differential Revision: D3548077 fbshipit-source-id: 49d3d83 --- infer/src/IR/Sil.re | 40 +++------------- infer/src/IR/Sil.rei | 17 +------ infer/src/IR/Unop.re | 48 +++++++++++++++++++ infer/src/IR/Unop.rei | 35 ++++++++++++++ infer/src/backend/dom.ml | 4 +- infer/src/backend/interproc.ml | 4 +- infer/src/backend/match.ml | 2 +- infer/src/backend/modelBuiltins.ml | 2 +- infer/src/backend/prop.ml | 50 ++++++++++---------- infer/src/backend/symExec.ml | 4 +- infer/src/checkers/annotationReachability.ml | 2 +- infer/src/checkers/checkTraceCallSequence.ml | 4 +- infer/src/checkers/codeQuery.ml | 4 +- infer/src/clang/cArithmetic_trans.ml | 6 +-- infer/src/eradicate/typeCheck.ml | 10 ++-- infer/src/java/jTrans.ml | 4 +- infer/src/java/jTransExn.ml | 3 +- infer/src/unit/analyzerTester.ml | 2 +- 18 files changed, 142 insertions(+), 99 deletions(-) create mode 100644 infer/src/IR/Unop.re create mode 100644 infer/src/IR/Unop.rei diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index 3c8cd29e9..6747c09d2 100644 --- a/infer/src/IR/Sil.re +++ b/infer/src/IR/Sil.re @@ -37,13 +37,6 @@ let get_sentinel_func_attribute_value attr_list => }; -/** Unary operations */ -type unop = - | Neg /** Unary minus */ - | BNot /** Bitwise complement (~) */ - | LNot /** Logical Not (!) */; - - /** Binary operations */ type binop = | PlusA /** arithmetic + */ @@ -427,7 +420,7 @@ type dexp = | Ddot of dexp Ident.fieldname | Dpvar of Pvar.t | Dpvaraddr of Pvar.t - | Dunop of unop dexp + | Dunop of Unop.t dexp | Dunknown | Dretcall of dexp (list dexp) Location.t call_flags; @@ -477,7 +470,7 @@ and exp = /** Pure variable: it is not an lvalue */ | Var of Ident.t /** Unary operator with type of the result if known */ - | UnOp of unop exp (option Typ.t) + | UnOp of Unop.t exp (option Typ.t) /** Binary operator */ | BinOp of binop exp exp /** Exception */ @@ -714,19 +707,6 @@ let exp_is_this = | Lvar pvar => Pvar.is_this pvar | _ => false; -let unop_compare o1 o2 => - switch (o1, o2) { - | (Neg, Neg) => 0 - | (Neg, _) => (-1) - | (_, Neg) => 1 - | (BNot, BNot) => 0 - | (BNot, _) => (-1) - | (_, BNot) => 1 - | (LNot, LNot) => 0 - }; - -let unop_equal o1 o2 => unop_compare o1 o2 == 0; - let binop_compare o1 o2 => switch (o1, o2) { | (PlusA, PlusA) => 0 @@ -1062,7 +1042,7 @@ let rec exp_compare (e1: exp) (e2: exp) :int => | (Var _, _) => (-1) | (_, Var _) => 1 | (UnOp o1 e1 to1, UnOp o2 e2 to2) => - let n = unop_compare o1 o2; + let n = Unop.compare o1 o2; if (n != 0) { n } else { @@ -1509,14 +1489,6 @@ let text_binop = | PtrFld => "_ptrfld_"; -/** String representation of unary operator. */ -let str_unop = - fun - | Neg => "-" - | BNot => "~" - | LNot => "!"; - - /** Pretty print a binary operator. */ let str_binop pe binop => switch pe.pe_kind { @@ -1628,7 +1600,7 @@ let rec dexp_to_string = }; ampersand ^ s } - | Dunop op de => str_unop op ^ dexp_to_string de + | Dunop op de => Unop.str op ^ dexp_to_string de | Dsizeof typ _ _ => pp_to_string (Typ.pp_full pe_text) typ | Dunknown => "unknown" | Dretcall de _ _ _ => "returned by " ^ dexp_to_string de; @@ -1756,7 +1728,7 @@ let rec _pp_exp pe0 pp_t f e0 => { | Var id => (Ident.pp pe) f id | Const c => F.fprintf f "%a" (Const.pp pe) c | Cast typ e => F.fprintf f "(%a)%a" pp_t typ pp_exp e - | UnOp op e _ => F.fprintf f "%s%a" (str_unop op) pp_exp e + | UnOp op e _ => F.fprintf f "%s%a" (Unop.str op) pp_exp e | BinOp op (Const c) e2 when Config.smt_output => print_binop_stm_output (Const c) op e2 | BinOp op e1 e2 => F.fprintf f "(%a %s %a)" pp_exp e1 (str_binop pe op) pp_exp e2 | Exn e => F.fprintf f "EXN %a" pp_exp e @@ -3663,7 +3635,7 @@ let rec exp_compare_structural e1 e2 exp_map => { switch (e1, e2) { | (Var _, Var _) => compare_exps_with_map e1 e2 exp_map | (UnOp o1 e1 to1, UnOp o2 e2 to2) => - let n = unop_compare o1 o2; + let n = Unop.compare o1 o2; if (n != 0) { (n, exp_map) } else { diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei index dd9b151bd..163bc7f29 100644 --- a/infer/src/IR/Sil.rei +++ b/infer/src/IR/Sil.rei @@ -26,13 +26,6 @@ type func_attribute = | FA_sentinel of int int; type access = | Default | Public | Private | Protected; -/** Unary operations */ -type unop = - | Neg /** Unary minus */ - | BNot /** Bitwise complement (~) */ - | LNot /** Logical Not (!) */; - - /** Binary operations */ type binop = | PlusA /** arithmetic + */ @@ -154,7 +147,7 @@ type dexp = | Ddot of dexp Ident.fieldname | Dpvar of Pvar.t | Dpvaraddr of Pvar.t - | Dunop of unop dexp + | Dunop of Unop.t dexp | Dunknown | Dretcall of dexp (list dexp) Location.t call_flags; @@ -204,7 +197,7 @@ and exp = /** Pure variable: it is not an lvalue */ | Var of Ident.t /** Unary operator with type of the result if known */ - | UnOp of unop exp (option Typ.t) + | UnOp of Unop.t exp (option Typ.t) /** Binary operator */ | BinOp of binop exp exp /** Exception */ @@ -489,8 +482,6 @@ let block_pvar: Pvar.t; /** Check if a pvar is a local pointing to a block in objc */ let is_block_pvar: Pvar.t => bool; -let unop_equal: unop => unop => bool; - let binop_equal: binop => binop => bool; @@ -621,10 +612,6 @@ let color_pre_wrapper: printenv => F.formatter => 'a => (printenv, bool); let color_post_wrapper: bool => printenv => F.formatter => unit; -/** String representation of a unary operator. */ -let str_unop: unop => string; - - /** String representation of a binary operator. */ let str_binop: printenv => binop => string; diff --git a/infer/src/IR/Unop.re b/infer/src/IR/Unop.re new file mode 100644 index 000000000..65855b81e --- /dev/null +++ b/infer/src/IR/Unop.re @@ -0,0 +1,48 @@ +/* + * vim: set ft=rust: + * vim: set ft=reason: + * + * Copyright (c) 2009 - 2013 Monoidics ltd. + * Copyright (c) 2013 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +open! Utils; + + +/** The Smallfoot Intermediate Language: Unary Operators */ +let module L = Logging; + +let module F = Format; + + +/** Unary operations */ +type t = + | Neg /** Unary minus */ + | BNot /** Bitwise complement (~) */ + | LNot /** Logical Not (!) */; + +let compare o1 o2 => + switch (o1, o2) { + | (Neg, Neg) => 0 + | (Neg, _) => (-1) + | (_, Neg) => 1 + | (BNot, BNot) => 0 + | (BNot, _) => (-1) + | (_, BNot) => 1 + | (LNot, LNot) => 0 + }; + +let equal o1 o2 => compare o1 o2 == 0; + + +/** String representation of unary operator. */ +let str = + fun + | Neg => "-" + | BNot => "~" + | LNot => "!"; diff --git a/infer/src/IR/Unop.rei b/infer/src/IR/Unop.rei new file mode 100644 index 000000000..2f45bb1dd --- /dev/null +++ b/infer/src/IR/Unop.rei @@ -0,0 +1,35 @@ +/* + * vim: set ft=rust: + * vim: set ft=reason: + * + * Copyright (c) 2009 - 2013 Monoidics ltd. + * Copyright (c) 2013 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +open! Utils; + + +/** The Smallfoot Intermediate Language: Unary Operators */ +let module L = Logging; + +let module F = Format; + + +/** Unary operations */ +type t = + | Neg /** Unary minus */ + | BNot /** Bitwise complement (~) */ + | LNot /** Logical Not (!) */; + +let equal: t => t => bool; + +let compare: t => t => int; + + +/** String representation of a unary operator. */ +let str: t => string; diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index 0671a8d29..7c47d2962 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -937,7 +937,7 @@ let rec exp_partial_join (e1: Sil.exp) (e2: Sil.exp) : Sil.exp = let e1'' = exp_partial_join e1 e2 in Sil.Cast (t1, e1'') | Sil.UnOp(unop1, e1, topt1), Sil.UnOp(unop2, e2, _) -> - if not (Sil.unop_equal unop1 unop2) then (L.d_strln "failure reason 23"; raise IList.Fail) + if not (Unop.equal unop1 unop2) then (L.d_strln "failure reason 23"; raise IList.Fail) else Sil.UnOp (unop1, exp_partial_join e1 e2, topt1) (* should be topt1 = topt2 *) | Sil.BinOp(Sil.PlusPI, e1, e1'), Sil.BinOp(Sil.PlusPI, e2, e2') -> let e1'' = exp_partial_join e1 e2 in @@ -1018,7 +1018,7 @@ let rec exp_partial_meet (e1: Sil.exp) (e2: Sil.exp) : Sil.exp = let e1'' = exp_partial_meet e1 e2 in Sil.Cast (t1, e1'') | Sil.UnOp(unop1, e1, topt1), Sil.UnOp(unop2, e2, _) -> - if not (Sil.unop_equal unop1 unop2) then (L.d_strln "failure reason 31"; raise IList.Fail) + if not (Unop.equal unop1 unop2) then (L.d_strln "failure reason 31"; raise IList.Fail) else Sil.UnOp (unop1, exp_partial_meet e1 e2, topt1) (* should be topt1 = topt2 *) | Sil.BinOp(binop1, e1, e1'), Sil.BinOp(binop2, e2, e2') -> if not (Sil.binop_equal binop1 binop2) then (L.d_strln "failure reason 32"; raise IList.Fail) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 9a5a295da..73ae9a3d2 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -400,7 +400,7 @@ let check_assignement_guard node = let leti = IList.filter is_letderef_instr ins in match pi, leti with | [Sil.Prune (Sil.Var(e1), _, _, _)], [Sil.Letderef(e2, e', _, _)] - | [Sil.Prune (Sil.UnOp(Sil.LNot, Sil.Var(e1), _), _, _, _)], + | [Sil.Prune (Sil.UnOp(Unop.LNot, Sil.Var(e1), _), _, _, _)], [Sil.Letderef(e2, e', _, _)] when (Ident.equal e1 e2) -> if verbose @@ -430,7 +430,7 @@ let check_assignement_guard node = let succs_have_simple_guards () = let check_instr = function | Sil.Prune (Sil.Var _, _, _, _) -> true - | Sil.Prune (Sil.UnOp(Sil.LNot, Sil.Var _, _), _, _, _) -> true + | Sil.Prune (Sil.UnOp(Unop.LNot, Sil.Var _, _), _, _, _) -> true | Sil.Prune _ -> false | _ -> true in let check_guard n = diff --git a/infer/src/backend/match.ml b/infer/src/backend/match.ml index 8c81e94e6..0d83cab86 100644 --- a/infer/src/backend/match.ml +++ b/infer/src/backend/match.ml @@ -58,7 +58,7 @@ let rec exp_match e1 sub vars e2 : (Sil.subst * Ident.t list) option = exp_match e1' sub vars e2' | Sil.Cast _, _ | _, Sil.Cast _ -> None - | Sil.UnOp(o1, e1', _), Sil.UnOp(o2, e2', _) when Sil.unop_equal o1 o2 -> + | Sil.UnOp(o1, e1', _), Sil.UnOp(o2, e2', _) when Unop.equal o1 o2 -> exp_match e1' sub vars e2' | Sil.UnOp _, _ | _, Sil.UnOp _ -> None (* Naive *) diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index 273c99705..6fa9c1901 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/infer/src/backend/modelBuiltins.ml @@ -180,7 +180,7 @@ let create_type tenv n_lexp typ prop = prop'' | None -> prop in let sil_is_null = Sil.BinOp (Sil.Eq, n_lexp, Sil.exp_zero) in - let sil_is_nonnull = Sil.UnOp (Sil.LNot, sil_is_null, None) in + let sil_is_nonnull = Sil.UnOp (Unop.LNot, sil_is_null, None) in let null_case = Propset.to_proplist (prune ~positive:true sil_is_null prop) in let non_null_case = Propset.to_proplist (prune ~positive:true sil_is_nonnull prop_type) in if ((IList.length non_null_case) > 0) && (!Config.footprint) then diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 803ec9214..5222d656f 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -466,41 +466,41 @@ let sym_eval abs e = e | Sil.Cast (_, e1) -> eval e1 - | Sil.UnOp (Sil.LNot, e1, topt) -> + | Sil.UnOp (Unop.LNot, e1, topt) -> begin match eval e1 with | Sil.Const (Const.Cint i) when IntLit.iszero i -> Sil.exp_one | Sil.Const (Const.Cint _) -> Sil.exp_zero - | Sil.UnOp(Sil.LNot, e1', _) -> + | Sil.UnOp(Unop.LNot, e1', _) -> e1' | e1' -> - if abs then Sil.exp_get_undefined false else Sil.UnOp(Sil.LNot, e1', topt) + if abs then Sil.exp_get_undefined false else Sil.UnOp(Unop.LNot, e1', topt) end - | Sil.UnOp (Sil.Neg, e1, topt) -> + | Sil.UnOp (Unop.Neg, e1, topt) -> begin match eval e1 with - | Sil.UnOp (Sil.Neg, e2', _) -> + | Sil.UnOp (Unop.Neg, e2', _) -> e2' | Sil.Const (Const.Cint i) -> Sil.exp_int (IntLit.neg i) | Sil.Const (Const.Cfloat v) -> Sil.exp_float (-. v) | Sil.Var id -> - Sil.UnOp (Sil.Neg, Sil.Var id, topt) + Sil.UnOp (Unop.Neg, Sil.Var id, topt) | e1' -> - if abs then Sil.exp_get_undefined false else Sil.UnOp (Sil.Neg, e1', topt) + if abs then Sil.exp_get_undefined false else Sil.UnOp (Unop.Neg, e1', topt) end - | Sil.UnOp (Sil.BNot, e1, topt) -> + | Sil.UnOp (Unop.BNot, e1, topt) -> begin match eval e1 with - | Sil.UnOp(Sil.BNot, e2', _) -> + | Sil.UnOp(Unop.BNot, e2', _) -> e2' | Sil.Const (Const.Cint i) -> Sil.exp_int (IntLit.lognot i) | e1' -> - if abs then Sil.exp_get_undefined false else Sil.UnOp (Sil.BNot, e1', topt) + if abs then Sil.exp_get_undefined false else Sil.UnOp (Unop.BNot, e1', topt) end | Sil.BinOp (Sil.Le, e1, e2) -> begin @@ -629,8 +629,8 @@ let sym_eval abs e = Sil.exp_int (n ++ m) | Sil.Const (Const.Cfloat v), Sil.Const (Const.Cfloat w) -> Sil.exp_float (v +. w) - | Sil.UnOp(Sil.Neg, f1, _), f2 - | f2, Sil.UnOp(Sil.Neg, f1, _) -> + | Sil.UnOp(Unop.Neg, f1, _), f2 + | f2, Sil.UnOp(Unop.Neg, f1, _) -> Sil.BinOp (ominus, f2, f1) | Sil.BinOp (Sil.PlusA, e, Sil.Const (Const.Cint n1)), Sil.Const (Const.Cint n2) | Sil.BinOp (Sil.PlusPI, e, Sil.Const (Const.Cint n1)), Sil.Const (Const.Cint n2) @@ -666,14 +666,14 @@ let sym_eval abs e = else begin match e1', e2' with | Sil.Const c, _ when iszero_int_float c -> - eval (Sil.UnOp(Sil.Neg, e2', None)) + eval (Sil.UnOp(Unop.Neg, e2', None)) | _, Sil.Const c when iszero_int_float c -> e1' | Sil.Const (Const.Cint n), Sil.Const (Const.Cint m) -> Sil.exp_int (n -- m) | Sil.Const (Const.Cfloat v), Sil.Const (Const.Cfloat w) -> Sil.exp_float (v -. w) - | _, Sil.UnOp (Sil.Neg, f2, _) -> + | _, Sil.UnOp (Unop.Neg, f2, _) -> eval (e1 +++ f2) | _ , Sil.Const(Const.Cint n) -> eval (e1' +++ (Sil.exp_int (IntLit.neg n))) @@ -697,13 +697,13 @@ let sym_eval abs e = | Sil.Const c, _ when isone_int_float c -> e2' | Sil.Const c, _ when isminusone_int_float c -> - eval (Sil.UnOp (Sil.Neg, e2', None)) + eval (Sil.UnOp (Unop.Neg, e2', None)) | _, Sil.Const c when iszero_int_float c -> Sil.exp_zero | _, Sil.Const c when isone_int_float c -> e1' | _, Sil.Const c when isminusone_int_float c -> - eval (Sil.UnOp (Sil.Neg, e1', None)) + eval (Sil.UnOp (Unop.Neg, e1', None)) | Sil.Const (Const.Cint n), Sil.Const (Const.Cint m) -> Sil.exp_int (IntLit.mul n m) | Sil.Const (Const.Cfloat v), Sil.Const (Const.Cfloat w) -> @@ -891,7 +891,7 @@ let mk_inequality e = let new_offset = Sil.exp_int (n' -- n -- IntLit.one) in let new_e = Sil.BinOp (Sil.Lt, new_offset, base') in Sil.Aeq (new_e, Sil.exp_one) - | Sil.UnOp(Sil.Neg, new_base, _) -> + | Sil.UnOp(Unop.Neg, new_base, _) -> (* In this case, base = -new_base. Construct -n-1 < new_base. *) let new_offset = Sil.exp_int (IntLit.zero -- n -- IntLit.one) in let new_e = Sil.BinOp (Sil.Lt, new_offset, new_base) in @@ -917,7 +917,7 @@ let mk_inequality e = let new_offset = Sil.exp_int (n' -- n -- IntLit.one) in let new_e = Sil.BinOp (Sil.Le, base', new_offset) in Sil.Aeq (new_e, Sil.exp_one) - | Sil.UnOp(Sil.Neg, new_base, _) -> + | Sil.UnOp(Unop.Neg, new_base, _) -> (* In this case, base = -new_base. Construct new_base <= -n-1 *) let new_offset = Sil.exp_int (IntLit.zero -- n -- IntLit.one) in let new_e = Sil.BinOp (Sil.Le, new_base, new_offset) in @@ -942,7 +942,7 @@ let inequality_normalize a = let pos1, neg1, n1 = exp_to_posnegoff e1 in let pos2, neg2, n2 = exp_to_posnegoff e2 in (pos1@neg2, neg1@pos2, n1 -- n2) - | Sil.UnOp(Sil.Neg, e1, _) -> + | Sil.UnOp(Unop.Neg, e1, _) -> let pos1, neg1, n1 = exp_to_posnegoff e1 in (neg1, pos1, IntLit.zero -- n1) | _ -> [e],[], IntLit.zero in @@ -1015,8 +1015,8 @@ let atom_normalize sub a0 = | _ -> eq in let handle_unary_negation e1 e2 = match e1, e2 with - | Sil.UnOp (Sil.LNot, e1', _), Sil.Const (Const.Cint i) - | Sil.Const (Const.Cint i), Sil.UnOp (Sil.LNot, e1', _) when IntLit.iszero i -> + | Sil.UnOp (Unop.LNot, e1', _), Sil.Const (Const.Cint i) + | Sil.Const (Const.Cint i), Sil.UnOp (Unop.LNot, e1', _) when IntLit.iszero i -> (e1', Sil.exp_zero, true) | _ -> (e1, e2, false) in let handle_boolean_operation from_equality e1 e2 = @@ -1974,7 +1974,7 @@ let find_arithmetic_problem proc_node_session prop exp = false in let rec walk = function | Sil.Var _ -> () - | Sil.UnOp (Sil.Neg, e, Some ( + | Sil.UnOp (Unop.Neg, e, Some ( (Typ.Tint (Typ.IUChar | Typ.IUInt | Typ.IUShort | Typ.IULong | Typ.IULongLong) as typ))) -> uminus_unsigned := (e, typ) :: !uminus_unsigned @@ -2779,8 +2779,8 @@ let trans_land_lor op ((idl1, stml1), e1) ((idl2, stml2), e2) loc = let id = Ident.create_fresh Ident.knormal in let prune_instr1, prune_res1, prune_instr2, prune_res2 = let cond1, cond2, res = match op with - | Sil.LAnd -> e1, Sil.UnOp(Sil.LNot, e1, None), IntLit.zero - | Sil.LOr -> Sil.UnOp(Sil.LNot, e1, None), e1, IntLit.one + | Sil.LAnd -> e1, Sil.UnOp(Unop.LNot, e1, None), IntLit.zero + | Sil.LOr -> Sil.UnOp(Unop.LNot, e1, None), e1, IntLit.one | _ -> assert false in let cond_res1 = Sil.BinOp(Sil.Eq, Sil.Var id, e2) in let cond_res2 = Sil.BinOp(Sil.Eq, Sil.Var id, Sil.exp_int res) in @@ -2836,7 +2836,7 @@ let trans_if_then_else ((idl1, stml1), e1) ((idl2, stml2), e2) ((idl3, stml3), e | Sil.Const (Const.Cint i) when IntLit.iszero i -> (idl1@idl3, stml1@stml3), e3 | Sil.Const (Const.Cint _) -> (idl1@idl2, stml1@stml2), e2 | _ -> - let e1not = Sil.UnOp(Sil.LNot, e1, None) in + let e1not = Sil.UnOp(Unop.LNot, e1, None) in let id = Ident.create_fresh Ident.knormal in let mk_prune_res e = let mk_prune cond = Sil.Prune (cond, loc, true, Sil.Ik_land_lor) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index fe0beec6a..59bbd49bb 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -324,7 +324,7 @@ let rec prune ~positive condition prop = assert false | Sil.Cast (_, condition') -> prune ~positive condition' prop - | Sil.UnOp (Sil.LNot, condition', _) -> + | Sil.UnOp (Unop.LNot, condition', _) -> prune ~positive:(not positive) condition' prop | Sil.UnOp _ -> assert false @@ -445,7 +445,7 @@ let check_already_dereferenced pname cond prop = let rec is_check_zero = function | Sil.Var id -> Some id - | Sil.UnOp(Sil.LNot, e, _) -> + | Sil.UnOp(Unop.LNot, e, _) -> is_check_zero e | Sil.BinOp ((Sil.Eq | Sil.Ne), Sil.Const Const.Cint i, Sil.Var id) | Sil.BinOp ((Sil.Eq | Sil.Ne), Sil.Var id, Sil.Const Const.Cint i) when IntLit.iszero i -> diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 0f205fae0..dffd6a30c 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -291,7 +291,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Sil.BinOp (Sil.Eq, lhs, rhs) when is_tracking_exp astate lhs -> Sil.exp_equal rhs Sil.exp_one - | Sil.UnOp (Sil.LNot, Sil.BinOp (Sil.Eq, lhs, rhs), _) + | Sil.UnOp (Unop.LNot, Sil.BinOp (Sil.Eq, lhs, rhs), _) when is_tracking_exp astate lhs -> Sil.exp_equal rhs Sil.exp_zero | _ -> diff --git a/infer/src/checkers/checkTraceCallSequence.ml b/infer/src/checkers/checkTraceCallSequence.ml index f1f51dbbe..bd8c1da29 100644 --- a/infer/src/checkers/checkTraceCallSequence.ml +++ b/infer/src/checkers/checkTraceCallSequence.ml @@ -244,9 +244,9 @@ module BooleanVars = struct (** Normalize a boolean condition. *) let normalize_condition cond_e = match cond_e with - | Sil.UnOp (Sil.LNot, Sil.BinOp (Sil.Eq, e1, e2), _) -> + | Sil.UnOp (Unop.LNot, Sil.BinOp (Sil.Eq, e1, e2), _) -> Sil.BinOp (Sil.Ne, e1, e2) - | Sil.UnOp (Sil.LNot, Sil.BinOp (Sil.Ne, e1, e2), _) -> + | Sil.UnOp (Unop.LNot, Sil.BinOp (Sil.Ne, e1, e2), _) -> Sil.BinOp (Sil.Eq, e1, e2) | _ -> cond_e in diff --git a/infer/src/checkers/codeQuery.ml b/infer/src/checkers/codeQuery.ml index 0d0a4dc37..5e866a723 100644 --- a/infer/src/checkers/codeQuery.ml +++ b/infer/src/checkers/codeQuery.ml @@ -127,9 +127,9 @@ module Match = struct let e1 = Idenv.expand_expr idenv _e1 in let e2 = Idenv.expand_expr idenv _e2 in binop_match bop op && exp_match env ae1 (Vval e1) && exp_match env ae2 (Vval e2) - | Sil.UnOp (Sil.LNot, (Sil.BinOp (Sil.Eq, e1, e2)), _) -> + | Sil.UnOp (Unop.LNot, (Sil.BinOp (Sil.Eq, e1, e2)), _) -> cond_match env idenv (Sil.BinOp (Sil.Ne, e1, e2)) (ae1, op, ae2) - | Sil.UnOp (Sil.LNot, (Sil.BinOp (Sil.Ne, e1, e2)), _) -> + | Sil.UnOp (Unop.LNot, (Sil.BinOp (Sil.Ne, e1, e2)), _) -> cond_match env idenv (Sil.BinOp (Sil.Eq, e1, e2)) (ae1, op, ae2) | _ -> false diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml index 3ed6cf7a0..25614dfbd 100644 --- a/infer/src/clang/cArithmetic_trans.ml +++ b/infer/src/clang/cArithmetic_trans.ml @@ -169,10 +169,10 @@ let unary_operation_instruction uoi e typ loc = else e_minus_1 in (exp, instr1::[Sil.Set (e, typ, e_minus_1, loc)]) - | `Not -> (un_exp (Sil.BNot), []) - | `Minus -> (un_exp (Sil.Neg), []) + | `Not -> (un_exp (Unop.BNot), []) + | `Minus -> (un_exp (Unop.Neg), []) | `Plus -> (e, []) - | `LNot -> (un_exp (Sil.LNot), []) + | `LNot -> (un_exp (Unop.LNot), []) | `Deref -> (* Actual dereferencing is handled by implicit cast from rvalue to lvalue *) (e, []) diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index 6853b9b1d..fa4cad14d 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -123,7 +123,7 @@ module ComplexExpressions = struct | Sil.Dpvaraddr _ (* front-end variable -- this should not happen) *) -> case_not_handled () | Sil.Dunop (op, de) -> - Sil.str_unop op ^ dexp_to_string de + Unop.str op ^ dexp_to_string de | Sil.Dsizeof _ -> case_not_handled () | Sil.Dunknown -> @@ -1023,9 +1023,9 @@ let typecheck_instr else typestate2 end - | Sil.UnOp (Sil.LNot, (Sil.BinOp (Sil.Eq, e1, e2)), _) -> + | Sil.UnOp (Unop.LNot, (Sil.BinOp (Sil.Eq, e1, e2)), _) -> check_condition node' (Sil.BinOp (Sil.Ne, e1, e2)) - | Sil.UnOp (Sil.LNot, (Sil.BinOp (Sil.Ne, e1, e2)), _) -> + | Sil.UnOp (Unop.LNot, (Sil.BinOp (Sil.Ne, e1, e2)), _) -> check_condition node' (Sil.BinOp (Sil.Eq, e1, e2)) | _ -> typestate in @@ -1046,9 +1046,9 @@ let typecheck_instr (** Normalize the condition by resolving temp variables. *) let rec normalize_cond _node _cond = match _cond with - | Sil.UnOp (Sil.LNot, c, top) -> + | Sil.UnOp (Unop.LNot, c, top) -> let node', c' = normalize_cond _node c in - node', Sil.UnOp (Sil.LNot, c', top) + node', Sil.UnOp (Unop.LNot, c', top) | Sil.BinOp (bop, c1, c2) -> let node', c1' = normalize_cond _node c1 in let node'', c2' = normalize_cond node' c2 in diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 8da6bf844..518f09fb5 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -438,7 +438,7 @@ let rec expression context pc expr = let (instrs, sil_ex, _) = expression context pc ex in begin match unop with - | JBir.Neg _ -> (instrs, Sil.UnOp (Sil.Neg, sil_ex, Some type_of_expr), type_of_expr) + | JBir.Neg _ -> (instrs, Sil.UnOp (Unop.Neg, sil_ex, Some type_of_expr), type_of_expr) | JBir.ArrayLength -> let array_typ_no_ptr = match type_of_ex with @@ -874,7 +874,7 @@ let rec instruction context pc instr : translation = and (instrs2, sil_ex2, _) = expression context pc e2 in let sil_op = get_test_operator op in let sil_test_false = Sil.BinOp (sil_op, sil_ex1, sil_ex2) in - let sil_test_true = Sil.UnOp(Sil.LNot, sil_test_false, None) in + let sil_test_true = Sil.UnOp(Unop.LNot, sil_test_false, None) in let sil_instrs_true = Sil.Prune (sil_test_true, loc, true, Sil.Ik_if) in let sil_instrs_false = Sil.Prune (sil_test_false, loc, false, Sil.Ik_if) in let node_kind_true = Cfg.Node.Prune_node (true, Sil.Ik_if, "method_body") in diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml index 3b64ace1f..f3302ffc1 100644 --- a/infer/src/java/jTransExn.ml +++ b/infer/src/java/jTransExn.ml @@ -73,7 +73,8 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table = Sil.Call ([id_instanceof], instanceof_builtin, args, loc, Sil.cf_default) in let if_kind = Sil.Ik_switch in let instr_prune_true = Sil.Prune (Sil.Var id_instanceof, loc, true, if_kind) in - let instr_prune_false = Sil.Prune (Sil.UnOp(Sil.LNot, Sil.Var id_instanceof, None), loc, false, if_kind) in + let instr_prune_false = + Sil.Prune (Sil.UnOp(Unop.LNot, Sil.Var id_instanceof, None), loc, false, if_kind) in let instr_set_catch_var = let catch_var = JContext.set_pvar context handler.JBir.e_catch_var ret_type in Sil.Set (Sil.Lvar catch_var, ret_type, Sil.Var id_exn_val, loc) in diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 0121548ad..9143862b0 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -165,7 +165,7 @@ module Make create_node (Cfg.Node.Prune_node (true_branch, if_kind, "")) [prune_instr] in let true_prune_node = mk_prune_node cond_exp if_kind true in let false_prune_node = - let negated_cond_exp = Sil.UnOp (Sil.LNot, cond_exp, None) in + let negated_cond_exp = Sil.UnOp (Unop.LNot, cond_exp, None) in mk_prune_node negated_cond_exp if_kind false in true_prune_node, false_prune_node in