diff options
Diffstat (limited to 'cil.patch/cabs2cil.ml.patch')
| -rw-r--r-- | cil.patch/cabs2cil.ml.patch | 325 |
1 files changed, 325 insertions, 0 deletions
diff --git a/cil.patch/cabs2cil.ml.patch b/cil.patch/cabs2cil.ml.patch new file mode 100644 index 00000000..12a81ca5 --- /dev/null +++ b/cil.patch/cabs2cil.ml.patch @@ -0,0 +1,325 @@ +*** ../cil/src/frontc/cabs2cil.ml 2006-05-21 06:14:15.000000000 +0200 +--- ../cil_patch/src/frontc/cabs2cil.ml 2006-07-25 10:45:51.136500945 +0200 +*************** +*** 1,3 **** +--- 1,7 ---- ++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) ++ (* MODIF: Return statement no longer added when the body of the function ++ falls-through. *) ++ + (* + * + * Copyright (c) 2001-2002, +*************** +*** 816,828 **** + (fun s -> + if s.labels != [] then + raise (Failure "cannot duplicate: has labels"); + (match s.skind with +! If _ | Switch _ | Loop _ | Block _ -> + raise (Failure "cannot duplicate: complex stmt") + | Instr il -> + pCount := !pCount + List.length il + | _ -> incr pCount); + if !pCount > 5 then raise (Failure ("cannot duplicate: too many instr")); + (* We can just copy it because there is nothing to share here. + * Except maybe for the ref cell in Goto but it is Ok to share + * that, I think *) +--- 820,835 ---- + (fun s -> + if s.labels != [] then + raise (Failure "cannot duplicate: has labels"); ++ (* + (match s.skind with +! If _ | Switch _ | (*Loop _*) +! While _ | DoWhile _ | For _ | Block _ -> + raise (Failure "cannot duplicate: complex stmt") + | Instr il -> + pCount := !pCount + List.length il + | _ -> incr pCount); + if !pCount > 5 then raise (Failure ("cannot duplicate: too many instr")); ++ *) + (* We can just copy it because there is nothing to share here. + * Except maybe for the ref cell in Goto but it is Ok to share + * that, I think *) +*************** +*** 838,843 **** +--- 845,851 ---- + let canDrop (c: chunk) = + List.for_all canDropStatement c.stmts + ++ (* + let loopChunk (body: chunk) : chunk = + (* Make the statement *) + let loop = mkStmt (Loop (c2block body, !currentLoc, None, None)) in +*************** +*** 845,850 **** +--- 853,885 ---- + postins = []; + cases = body.cases; + } ++ *) ++ ++ let whileChunk (e: exp) (body: chunk) : chunk = ++ let loop = mkStmt (While (e, c2block body, !currentLoc)) in ++ ++ { stmts = [ loop ]; ++ postins = []; ++ cases = body.cases; ++ } ++ ++ let doWhileChunk (e: exp) (body: chunk) : chunk = ++ let loop = mkStmt (DoWhile (e, c2block body, !currentLoc)) in ++ ++ { stmts = [ loop ]; ++ postins = []; ++ cases = body.cases; ++ } ++ ++ let forChunk (bInit: chunk) (e: exp) (bIter: chunk) ++ (body: chunk) : chunk = ++ let loop = mkStmt (For (c2block bInit, e, c2block bIter, ++ c2block body, !currentLoc)) in ++ ++ { stmts = [ loop ]; ++ postins = []; ++ cases = body.cases; ++ } + + let breakChunk (l: location) : chunk = + { stmts = [ mkStmt (Break l) ]; +*************** +*** 959,964 **** +--- 994,1000 ---- + + + (************ Labels ***********) ++ (* + (* Since we turn dowhile and for loops into while we need to take care in + * processing the continue statement. For each loop that we enter we place a + * marker in a list saying what kinds of loop it is. When we see a continue +*************** +*** 971,980 **** +--- 1007,1035 ---- + + let startLoop iswhile = + continues := (if iswhile then While else NotWhile (ref "")) :: !continues ++ *) ++ ++ (* We need to take care while processing the continue statement... ++ * For each loop that we enter we place a marker in a list saying what ++ * chunk of code we must duplicate before each continue statement ++ * in order to preserve the semantics. *) ++ type loopMarker = ++ DuplicateBeforeContinue of chunk ++ ++ let continues : loopMarker list ref = ref [] ++ ++ let startLoop lstate = ++ continues := lstate :: !continues ++ ++ let continueDuplicateChunk (l: location) : chunk = ++ match !continues with ++ | [] -> E.s (error "continue not in a loop") ++ | DuplicateBeforeContinue c :: _ -> c @@ continueChunk l + + (* Sometimes we need to create new label names *) + let newLabelName (base: string) = fst (newAlphaName false "label" base) + ++ (* + let continueOrLabelChunk (l: location) : chunk = + match !continues with + [] -> E.s (error "continue not in a loop") +*************** +*** 990,995 **** +--- 1045,1051 ---- + [] -> E.s (error "labContinue not in a loop") + | While :: rest -> c + | NotWhile lr :: rest -> if !lr = "" then c else consLabel !lr c !currentLoc false ++ *) + + let exitLoop () = + match !continues with +*************** +*** 5465,5473 **** +--- 5521,5534 ---- + * then the switch falls through. *) + blockFallsThrough b || blockCanBreak b + end ++ (* + | Loop (b, _, _, _) -> + (* A loop falls through if it can break. *) + blockCanBreak b ++ *) ++ | While (_, b, _) -> blockCanBreak b ++ | DoWhile (_, b, _) -> blockCanBreak b ++ | For (_, _, _, b, _) -> blockCanBreak b + | Block b -> blockFallsThrough b + | TryFinally (b, h, _) -> blockFallsThrough h + | TryExcept (b, _, h, _) -> true (* Conservative *) +*************** +*** 5512,5518 **** + | Break _ -> true + | If (_, b1, b2, _) -> + blockCanBreak b1 || blockCanBreak b2 +! | Switch _ | Loop _ -> + (* switches and loops catch any breaks in their bodies *) + false + | Block b -> blockCanBreak b +--- 5573,5579 ---- + | Break _ -> true + | If (_, b1, b2, _) -> + blockCanBreak b1 || blockCanBreak b2 +! | Switch _ | (*Loop _*) While _ | DoWhile _ | For _ -> + (* switches and loops catch any breaks in their bodies *) + false + | Block b -> blockCanBreak b +*************** +*** 5522,5527 **** +--- 5583,5589 ---- + List.exists stmtCanBreak b.bstmts + in + if blockFallsThrough !currentFunctionFDEC.sbody then begin ++ (* + let retval = + match unrollType !currentReturnType with + TVoid _ -> None +*************** +*** 5537,5542 **** +--- 5599,5605 ---- + !currentFunctionFDEC.sbody.bstmts <- + !currentFunctionFDEC.sbody.bstmts + @ [mkStmt (Return(retval, endloc))] ++ *) + end; + + (* ignore (E.log "The env after finishing the body of %s:\n%t\n" +*************** +*** 5738,5743 **** +--- 5801,5807 ---- + doCondition false e st' sf' + + | A.WHILE(e,s,loc) -> ++ (* + startLoop true; + let s' = doStatement s in + exitLoop (); +*************** +*** 5746,5753 **** +--- 5810,5836 ---- + loopChunk ((doCondition false e skipChunk + (breakChunk loc')) + @@ s') ++ *) ++ (** We need to convert A.WHILE(e,s) where e may have side effects ++ into Cil.While(e',s') where e' is side-effect free. *) ++ ++ (* Let e == (sCond , eCond) with sCond a sequence of statements ++ and eCond a side-effect free expression. *) ++ let (sCond, eCond, _) = doExp false e (AExp None) in ++ ++ (* Then doStatement(A.WHILE((sCond , eCond), s)) ++ = sCond ; Cil.While(eCond, (doStatement(s) ; sCond)) ++ where doStatement(A.CONTINUE) = (sCond ; Cil.Continue). *) ++ ++ startLoop (DuplicateBeforeContinue sCond); ++ let s' = doStatement s in ++ exitLoop (); ++ let loc' = convLoc loc in ++ currentLoc := loc'; ++ sCond @@ (whileChunk eCond (s' @@ sCond)) + + | A.DOWHILE(e,s,loc) -> ++ (* + startLoop false; + let s' = doStatement s in + let loc' = convLoc loc in +*************** +*** 5757,5764 **** + in + exitLoop (); + loopChunk (s' @@ s'') + +! | A.FOR(fc1,e2,e3,s,loc) -> begin + let loc' = convLoc loc in + currentLoc := loc'; + enterScope (); (* Just in case we have a declaration *) +--- 5840,5866 ---- + in + exitLoop (); + loopChunk (s' @@ s'') ++ *) ++ (** We need to convert A.DOWHILE(e,s) where e may have side effects ++ into Cil.DoWhile(e',s') where e' is side-effect free. *) ++ ++ (* Let e == (sCond , eCond) with sCond a sequence of statements ++ and eCond a side-effect free expression. *) ++ let (sCond, eCond, _) = doExp false e (AExp None) in ++ ++ (* Then doStatement(A.DOWHILE((sCond , eCond), s)) ++ = Cil.DoWhile(eCond, (doStatement(s) ; sCond)) ++ where doStatement(A.CONTINUE) = (sCond ; Cil.Continue). *) ++ ++ startLoop (DuplicateBeforeContinue sCond); ++ let s' = doStatement s in ++ exitLoop (); ++ let loc' = convLoc loc in ++ currentLoc := loc'; ++ doWhileChunk eCond (s' @@ sCond) + +! | A.FOR(fc1,e2,e3,s,loc) -> +! (*begin + let loc' = convLoc loc in + currentLoc := loc'; + enterScope (); (* Just in case we have a declaration *) +*************** +*** 5784,5789 **** +--- 5886,5920 ---- + exitScope (); + res + end ++ *) ++ (** We need to convert A.FOR(e1,e2,e3,s) where e1, e2 and e3 may ++ have side effects into Cil.For(bInit,e2',bIter,s') where e2' ++ is side-effect free. **) ++ ++ (* Let e1 == bInit be a block of statements ++ Let e2 == (bCond , eCond) with bCond a block of statements ++ and eCond a side-effect free expression ++ Let e3 == bIter be a sequence of statements. *) ++ let (bInit, _, _) = match fc1 with ++ | FC_EXP e1 -> doExp false e1 ADrop ++ | FC_DECL d1 -> (doDecl false d1, zero, voidType) in ++ let (bCond, eCond, _) = doExp false e2 (AExp None) in ++ let eCond' = match eCond with ++ | Const(CStr "exp_nothing") -> Cil.one ++ | _ -> eCond in ++ let (bIter, _, _) = doExp false e3 ADrop in ++ ++ (* Then doStatement(A.FOR(bInit, (bCond , eCond), bIter, s)) ++ = Cil.For({bInit; bCond}, eCond', bIter, {doStatement(s); bCond}) ++ where doStatement(A.CONTINUE) = (bCond ; Cil.Continue). *) ++ ++ startLoop (DuplicateBeforeContinue bCond); ++ let s' = doStatement s in ++ exitLoop (); ++ let loc' = convLoc loc in ++ currentLoc := loc'; ++ (forChunk (bInit @@ bCond) eCond' bIter (s' @@ bCond)) ++ + | A.BREAK loc -> + let loc' = convLoc loc in + currentLoc := loc'; +*************** +*** 5792,5798 **** +--- 5923,5932 ---- + | A.CONTINUE loc -> + let loc' = convLoc loc in + currentLoc := loc'; ++ (* + continueOrLabelChunk loc' ++ *) ++ continueDuplicateChunk loc' + + | A.RETURN (A.NOTHING, loc) -> + let loc' = convLoc loc in |