Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Add option removeBranchingOnConstants #103

Merged
merged 4 commits into from
Jul 18, 2022
Merged

Add option removeBranchingOnConstants #103

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
53c6fa8
Add option `removeBranchingOnConstants`
michael-schwarz Jul 15, 2022
1ef28fa
Do no remove branching on expressions if they are const
michael-schwarz Jul 18, 2022
2ebfe85
Consider `removeBranchingOnConstant` in `constFoldBinop`
michael-schwarz Jul 18, 2022
3ac01e5
Respect `asConst` when `removeBranchingOnConstants`
michael-schwarz Jul 18, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 7 additions & 4 deletions src/cil.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,9 @@ let envMachine : M.mach option ref = ref None
let lowerConstants: bool ref = ref true
(** Do lower constants (default true) *)

let removeBranchingOnConstants: bool ref = ref true
(** Remove branches of the form if(const) ... else ... (default true) *)

let insertImplicitCasts: bool ref = ref true
(** Do insert implicit casts (default true) *)

Expand Down Expand Up @@ -2694,10 +2697,10 @@ and constFoldBinOp (machdep: bool) bop e1 e2 tres =
| Lt, Some i1, Some i2 -> if compare_cilint i1 i2 < 0 then one else zero
| Gt, Some i1, Some i2 -> if compare_cilint i1 i2 > 0 then one else zero

| LAnd, Some i1, _ -> if is_zero_cilint i1 then collapse0 () else collapse e2'
| LAnd, _, Some i2 -> if is_zero_cilint i2 then collapse0 () else collapse e1'
| LOr, Some i1, _ -> if is_zero_cilint i1 then collapse e2' else one
| LOr, _, Some i2 -> if is_zero_cilint i2 then collapse e1' else one
| LAnd, Some i1, _ when !removeBranchingOnConstants -> if is_zero_cilint i1 then collapse0 () else collapse e2'
| LAnd, _, Some i2 when !removeBranchingOnConstants -> if is_zero_cilint i2 then collapse0 () else collapse e1'
| LOr, Some i1, _ when !removeBranchingOnConstants -> if is_zero_cilint i1 then collapse e2' else one
| LOr, _, Some i2 when !removeBranchingOnConstants -> if is_zero_cilint i2 then collapse e1' else one

| _ -> BinOp(bop, e1', e2', tres)
in
Expand Down
3 changes: 3 additions & 0 deletions src/cil.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1128,6 +1128,9 @@ and typsig =
val lowerConstants: bool ref
(** Do lower constants (default true) *)

val removeBranchingOnConstants: bool ref
(** Remove branches of the form if(const) ... else ... (default true) *)

val insertImplicitCasts: bool ref
(** Do insert implicit casts (default true) *)

Expand Down
74 changes: 35 additions & 39 deletions src/frontc/cabs2cil.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4242,30 +4242,28 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
let ce = doCondExp asconst e in
(* We must normalize the result to 0 or 1 *)
match ce with
CEExp (se, ((Const _) as c)) ->
finishExp se (if isConstTrue c then one else zero) intType
| CEExp (se, ((UnOp(LNot, _, _)|BinOp((Lt|Gt|Le|Ge|Eq|Ne|LAnd|LOr), _, _, _)) as e)) ->
(* already normalized to 0 or 1 *)
finishExp se e intType
| CEExp (se, ((Const _) as c)) -> finishExp se (if isConstTrue c then one else zero) intType
| CEExp (se, ((UnOp(LNot, _, _)|BinOp((Lt|Gt|Le|Ge|Eq|Ne|LAnd|LOr), _, _, _)) as e)) ->
(* already normalized to 0 or 1 *)
finishExp se e intType
| CEExp (se, e) ->
let e' =
let te = typeOf e in
let _, zte = castTo intType te zero in
BinOp(Ne, e, zte, intType)
in
finishExp se e' intType
let e' =
let te = typeOf e in
let _, zte = castTo intType te zero in
BinOp(Ne, e, zte, intType)
in
finishExp se e' intType
| _ ->
let tmp =
var (newTempVar (text "<boolean expression>") true intType)
in
finishExp (compileCondExp ce
(empty +++ (Set(tmp, integer 1,
!currentLoc, !currentExpLoc)))
(empty +++ (Set(tmp, integer 0,
!currentLoc, !currentExpLoc))))
(Lval tmp)
intType
end
let tmp = var (newTempVar (text "<boolean expression>") true intType)
in
finishExp (compileCondExp asconst ce
(empty +++ (Set(tmp, integer 1,
!currentLoc, !currentExpLoc)))
(empty +++ (Set(tmp, integer 0,
!currentLoc, !currentExpLoc))))
(Lval tmp)
intType
end

| A.CALL(f, args) ->
if asconst then ignore (warnOpt "CALL in constant");
Expand Down Expand Up @@ -4765,9 +4763,9 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
(* Compute the type of the result *)
let tresult = conditionalConversion t2 t3 e_of_t2 e3' in
match ce1 with
CEExp (se1, e1') when isConstFalse e1' && canDrop se2 ->
CEExp (se1, e1') when isConstFalse e1' && canDrop se2 && (!Cil.removeBranchingOnConstants || asconst) ->
finishExp (se1 @@ se3) (snd (castTo t3 tresult e3')) tresult
| CEExp (se1, e1') when isConstTrue e1' && canDrop se3 ->
| CEExp (se1, e1') when isConstTrue e1' && canDrop se3 && (!Cil.removeBranchingOnConstants || asconst) ->
begin
match e2'o with
None -> (* use e1' *)
Expand Down Expand Up @@ -5081,7 +5079,7 @@ and doCondExp (asconst: bool) (* Try to evaluate the conditional expression
let ce1 = doCondExp asconst e1 in
let ce2 = doCondExp asconst e2 in
match ce1, ce2 with
CEExp (se1, ((Const _) as ci1)), _ ->
| CEExp (se1, ((Const _) as ci1)), _ when (!Cil.removeBranchingOnConstants || asconst) ->
if isConstTrue ci1 then
addChunkBeforeCE se1 ce2
else
Expand All @@ -5090,8 +5088,7 @@ and doCondExp (asconst: bool) (* Try to evaluate the conditional expression
ce1
else
CEAnd (ce1, ce2)
| CEExp(se1, e1'), CEExp (se2, e2') when
!useLogicalOperators && isEmpty se2 ->
| CEExp(se1, e1'), CEExp (se2, e2') when !useLogicalOperators && isEmpty se2 ->
CEExp (se1, BinOp(LAnd, e1', e2', intType))
| _ -> CEAnd (ce1, ce2)
end
Expand All @@ -5100,7 +5097,7 @@ and doCondExp (asconst: bool) (* Try to evaluate the conditional expression
let ce1 = doCondExp asconst e1 in
let ce2 = doCondExp asconst e2 in
match ce1, ce2 with
CEExp (se1, (Const(CInt _) as ci1)), _ ->
| CEExp (se1, (Const(CInt _) as ci1)), _ when (!Cil.removeBranchingOnConstants || asconst) ->
if isConstFalse ci1 then
addChunkBeforeCE se1 ce2
else
Expand All @@ -5110,8 +5107,7 @@ and doCondExp (asconst: bool) (* Try to evaluate the conditional expression
else
CEOr (ce1, ce2)

| CEExp (se1, e1'), CEExp (se2, e2') when
!useLogicalOperators && isEmpty se2 ->
| CEExp (se1, e1'), CEExp (se2, e2') when !useLogicalOperators && isEmpty se2 ->
CEExp (se1, BinOp(LOr, e1', e2', intType))
| _ -> CEOr (ce1, ce2)
end
Expand All @@ -5137,7 +5133,7 @@ and doCondExp (asconst: bool) (* Try to evaluate the conditional expression
ignore (checkBool t e);
CEExp (se, if !lowerConstants then constFold asconst e else e)

and compileCondExp (ce: condExpRes) (st: chunk) (sf: chunk) : chunk =
and compileCondExp (asconst:bool) (ce: condExpRes) (st: chunk) (sf: chunk) : chunk =
match ce with
| CEAnd (ce1, ce2) ->
let (sf1, sf2) =
Expand All @@ -5147,9 +5143,9 @@ and compileCondExp (ce: condExpRes) (st: chunk) (sf: chunk) : chunk =
let lab = newLabelName "_L" in
(gotoChunk lab !currentLoc, consLabel lab sf !currentLoc false)
in
let st' = compileCondExp ce2 st sf1 in
let st' = compileCondExp asconst ce2 st sf1 in
let sf' = sf2 in
compileCondExp ce1 st' sf'
compileCondExp asconst ce1 st' sf'

| CEOr (ce1, ce2) ->
let (st1, st2) =
Expand All @@ -5160,15 +5156,15 @@ and compileCondExp (ce: condExpRes) (st: chunk) (sf: chunk) : chunk =
(gotoChunk lab !currentLoc, consLabel lab st !currentLoc false)
in
let st' = st1 in
let sf' = compileCondExp ce2 st2 sf in
compileCondExp ce1 st' sf'
let sf' = compileCondExp asconst ce2 st2 sf in
compileCondExp asconst ce1 st' sf'

| CENot ce1 -> compileCondExp ce1 sf st
| CENot ce1 -> compileCondExp asconst ce1 sf st

| CEExp (se, e) -> begin
match e with
Const(CInt(i,_,_)) when not (is_zero_cilint i) && canDrop sf -> se @@ st
| Const(CInt(z,_,_)) when is_zero_cilint z && canDrop st -> se @@ sf
Const(CInt(i,_,_)) when not (is_zero_cilint i) && canDrop sf && (!Cil.removeBranchingOnConstants || asconst)-> se @@ st
| Const(CInt(z,_,_)) when is_zero_cilint z && canDrop st && (!Cil.removeBranchingOnConstants || asconst) -> se @@ sf
| _ -> se @@ ifChunk e !currentLoc !currentExpLoc st sf
end

Expand All @@ -5182,7 +5178,7 @@ and doCondition (isconst: bool) (* If we are in constants, we do our best to
if isEmpty st && isEmpty sf then
let se,_,_ = doExp isconst e ADrop in se
else
compileCondExp (doCondExp isconst e) st sf
compileCondExp isconst (doCondExp isconst e) st sf

(* Returns pure expression if there exists one, None otherwise. *)
and doPureExp ?(asconst=true) (e : A.expression) : exp option =
Expand Down