path: root/cil.patch/cabs2cil.ml.patch

*** ../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