From 78fe475b1417402a4576084b4c00c309dbfc990f Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 6 Dec 2021 15:16:08 +0100 Subject: [PATCH 1/3] constFoldBinOp do not const fold if signed overflow --- src/cil.ml | 25 ++++++++++++++++++------- 1 file changed, 18 insertions(+), 7 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index c3a456122..dae98954a 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -2579,6 +2579,16 @@ and constFoldLval machdep (host,offset) = and constFoldBinOp (machdep: bool) bop e1 e2 tres = let e1' = constFold machdep e1 in let e2' = constFold machdep e2 in + let if_not_overflow fallback ik i = + if not (isSigned ik) then + kintegerCilint ik i + else + let i', trunc = truncateCilint ik i in + if trunc = NoTruncation then + kintegerCilint ik i + else + fallback + in if isIntegralType tres then begin let newe = let tk = @@ -2601,27 +2611,28 @@ and constFoldBinOp (machdep: bool) bop e1 e2 tres = with SizeOfError _ -> false else false in + let no_ov = if_not_overflow (BinOp(bop, e1', e2', tres)) tk in (* Assume that the necessary promotions have been done *) match bop, getInteger e1', getInteger e2' with - | PlusA, Some i1, Some i2 -> kintegerCilint tk (add_cilint i1 i2) + | PlusA, Some i1, Some i2 -> no_ov (add_cilint i1 i2) | PlusA, Some z, _ when is_zero_cilint z -> collapse e2' | PlusA, _, Some z when is_zero_cilint z -> collapse e1' - | MinusA, Some i1, Some i2 -> kintegerCilint tk (sub_cilint i1 i2) + | MinusA, Some i1, Some i2 -> no_ov (sub_cilint i1 i2) | MinusA, _, Some z when is_zero_cilint z -> collapse e1' - | Mult, Some i1, Some i2 -> kintegerCilint tk (mul_cilint i1 i2) + | Mult, Some i1, Some i2 -> no_ov (mul_cilint i1 i2) | Mult, Some z, _ when is_zero_cilint z -> collapse0 () | Mult, _, Some z when is_zero_cilint z -> collapse0 () | Mult, Some o, _ when compare_cilint o one_cilint = 0 -> collapse e2' | Mult, _, Some o when compare_cilint o one_cilint = 0 -> collapse e1' | Div, Some i1, Some i2 -> begin - try kintegerCilint tk (div0_cilint i1 i2) + try no_ov (div0_cilint i1 i2) with Division_by_zero -> BinOp(bop, e1', e2', tres) - end + end | Div, _, Some o when compare_cilint o one_cilint = 0 -> collapse e1' | Mod, Some i1, Some i2 -> begin - try kintegerCilint tk (rem_cilint i1 i2) + try no_ov (rem_cilint i1 i2) with Division_by_zero -> BinOp(bop, e1', e2', tres) - end + end | Mod, _, Some o when compare_cilint o one_cilint = 0 -> collapse0 () | BAnd, Some i1, Some i2 -> kintegerCilint tk (logand_cilint i1 i2) From 63acd3fe1864b61435fb4f57e5566e97e85c4430 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 20 Dec 2021 11:15:23 +0100 Subject: [PATCH 2/3] Also prevent overflows in constFold for unop --- src/cil.ml | 34 ++++++++++++++++++---------------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 38b0f781c..58e0a41af 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -2181,6 +2181,18 @@ let rec getInteger (e:exp) : cilint option = end | _ -> None +(** Return the (wrapped) constant i if it fits into ik without any signed overflow, + otherwise return fallback *) +let const_if_not_overflow fallback ik i = + if not (isSigned ik) then + kintegerCilint ik i + else + let i', trunc = truncateCilint ik i in + if trunc = NoTruncation then + kintegerCilint ik i + else + fallback + let isZero (e: exp) : bool = match getInteger e with | Some n -> is_zero_cilint n @@ -2518,16 +2530,16 @@ and constFold (machdep: bool) (e: exp) : exp = try let tk = match unrollType tres with - TInt(ik, _) -> ik + | TInt(ik, _) -> ik | TEnum (ei, _) -> ei.ekind | _ -> raise Not_found (* probably a float *) in match constFold machdep e1 with - Const(CInt(i,ik,_)) -> begin - let ic = mkCilintIk ik i in + | Const(CInt(i,ik,s)) -> begin + let ic = mkCilintIk ik i in match unop with - Neg -> kintegerCilint tk (neg_cilint ic) - | BNot -> kintegerCilint tk (lognot_cilint ic) + Neg -> const_if_not_overflow (UnOp(Neg,Const(CInt(i,ik,s)),tres)) tk (neg_cilint ic) + | BNot -> const_if_not_overflow (UnOp(BNot,Const(CInt(i,ik,s)),tres)) tk (lognot_cilint ic) | LNot -> if is_zero_cilint ic then one else zero end | e1c -> UnOp(unop, e1c, tres) @@ -2600,16 +2612,6 @@ and constFoldLval machdep (host,offset) = and constFoldBinOp (machdep: bool) bop e1 e2 tres = let e1' = constFold machdep e1 in let e2' = constFold machdep e2 in - let if_not_overflow fallback ik i = - if not (isSigned ik) then - kintegerCilint ik i - else - let i', trunc = truncateCilint ik i in - if trunc = NoTruncation then - kintegerCilint ik i - else - fallback - in if isIntegralType tres then begin let newe = let tk = @@ -2632,7 +2634,7 @@ and constFoldBinOp (machdep: bool) bop e1 e2 tres = with SizeOfError _ -> false else false in - let no_ov = if_not_overflow (BinOp(bop, e1', e2', tres)) tk in + let no_ov = const_if_not_overflow (BinOp(bop, e1', e2', tres)) tk in (* Assume that the necessary promotions have been done *) match bop, getInteger e1', getInteger e2' with | PlusA, Some i1, Some i2 -> no_ov (add_cilint i1 i2) From 1cea359df2d3ffdb4079d8221bba36ec956c6778 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 20 Dec 2021 15:16:22 +0100 Subject: [PATCH 3/3] Do not fold on overflow for CABS Unop --- src/cil.mli | 2 ++ src/frontc/cabs2cil.ml | 5 +++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/cil.mli b/src/cil.mli index b4afa6c7f..45e60e015 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -2584,6 +2584,8 @@ val mkCilint : ikind -> int64 -> cilint val mkCilintIk : ikind -> cilint -> cilint +val const_if_not_overflow : exp -> ikind -> cilint -> exp + (** The size of a type, in bytes. Returns a constant expression or a * "sizeof" expression if it cannot compute the size. This function * is architecture dependent, so you should only call this after you diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 015c74d45..48e2f02ac 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -3805,10 +3805,11 @@ and doExp (asconst: bool) (* This expression is used as a constant *) let (se, e', t) = doExp asconst e (AExp None) in if isIntegralType t then let tres = integralPromotion t in + let fallback = UnOp(Neg, makeCastT ~e:e' ~oldt:t ~newt:tres, tres) in let e'' = match e', tres with - | Const(CInt(i, _, _)), TInt(ik, _) -> kintegerCilint ik (neg_cilint i) - | _ -> UnOp(Neg, makeCastT ~e:e' ~oldt:t ~newt:tres, tres) + | Const(CInt(i, _, _)), TInt(ik, _) -> const_if_not_overflow fallback ik (neg_cilint i) + | _ -> fallback in finishExp se e'' tres else