Integration du front-end CIL developpe par Thomas Moniot

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 381 insertions, 0 deletions

diff --git a/cil.patch/cil.ml.patch b/cil.patch/cil.ml.patch
new file mode 100644
index 00000000..a49b73d1
--- /dev/null
+++ b/cil.patch/cil.ml.patch
@@ -0,0 +1,381 @@
+*** ../cil/src/cil.ml	2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/cil.ml	2006-07-25 10:57:30.686790845 +0200
+***************
+*** 1,3 ****
+--- 1,6 ----
++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
++ (* MODIF: useLogicalOperators flag set to true by default. *)
++ 
+  (*
+   *
+   * Copyright (c) 2001-2003,
+***************
+*** 63,69 ****
+                                         * print output for the MS VC 
+                                         * compiler. Default is GCC *)
+  
+! let useLogicalOperators = ref false
+  
+  
+  module M = Machdep
+--- 66,72 ----
+                                         * print output for the MS VC 
+                                         * compiler. Default is GCC *)
+  
+! let useLogicalOperators = ref (*false*) true
+  
+  
+  module M = Machdep
+***************
+*** 684,692 ****
+    | Goto of stmt ref * location         (** A goto statement. Appears from 
+                                              actual goto's in the code. *)
+    | Break of location                   (** A break to the end of the nearest 
+!                                              enclosing Loop or Switch *)
+    | Continue of location                (** A continue to the start of the 
+!                                             nearest enclosing [Loop] *)
+    | If of exp * block * block * location (** A conditional. 
+                                               Two successors, the "then" and 
+                                               the "else" branches. Both 
+--- 687,695 ----
+    | Goto of stmt ref * location         (** A goto statement. Appears from 
+                                              actual goto's in the code. *)
+    | Break of location                   (** A break to the end of the nearest 
+!                                              enclosing loop or Switch *)
+    | Continue of location                (** A continue to the start of the 
+!                                             nearest enclosing loop *)
+    | If of exp * block * block * location (** A conditional. 
+                                               Two successors, the "then" and 
+                                               the "else" branches. Both 
+***************
+*** 701,706 ****
+--- 704,710 ----
+                                             you can get from the labels of the 
+                                             statement *)
+  
++ (*
+    | Loop of block * location * (stmt option) * (stmt option) 
+                                             (** A [while(1)] loop. The 
+                                              * termination test is implemented 
+***************
+*** 713,718 ****
+--- 717,726 ----
+                                              * and the second will point to 
+                                              * the stmt containing the break 
+                                              * label for this loop. *)
++ *)
++   | While of exp * block * location                 (** A while loop. *)
++   | DoWhile of exp * block * location               (** A do...while loop. *)
++   | For of block * exp * block * block * location   (** A for loop. *)
+  
+    | Block of block                      (** Just a block of statements. Use it 
+                                              as a way to keep some attributes 
+***************
+*** 1040,1046 ****
+--- 1048,1059 ----
+      | Continue(loc) -> loc
+      | If(_, _, _, loc) -> loc
+      | Switch (_, _, _, loc) -> loc
++ (*
+      | Loop (_, loc, _, _) -> loc
++ *)
++     | While (_, _, loc) -> loc
++     | DoWhile (_, _, loc) -> loc
++     | For (_, _, _, _, loc) -> loc
+      | Block b -> if b.bstmts == [] then lu 
+                   else get_stmtLoc ((List.hd b.bstmts).skind)
+      | TryFinally (_, _, l) -> l
+***************
+*** 1524,1533 ****
+--- 1537,1549 ----
+  
+  let mkWhile ~(guard:exp) ~(body: stmt list) : stmt list = 
+    (* Do it like this so that the pretty printer recognizes it *)
++ (*
+    [ mkStmt (Loop (mkBlock (mkStmt (If(guard, 
+                                        mkBlock [ mkEmptyStmt () ], 
+                                        mkBlock [ mkStmt (Break lu)], lu)) ::
+                             body), lu, None, None)) ]
++ *)
++   [ mkStmt (While (guard, mkBlock body, lu)) ]
+  
+  
+  
+***************
+*** 3448,3453 ****
+--- 3464,3471 ----
+                  ++ self#pExp () e
+                  ++ text ") "
+                  ++ self#pBlock () b)
++ 
++ (*
+      | Loop(b, l, _, _) -> begin
+          (* Maybe the first thing is a conditional. Turn it into a WHILE *)
+          try
+***************
+*** 3484,3489 ****
+--- 3502,3540 ----
+                    ++ text "ile (1) "
+                    ++ self#pBlock () b)
+      end
++ *)
++ 
++     | While (e, b, l) ->
++         self#pLineDirective l
++           ++ (align
++                 ++ text "while ("
++                 ++ self#pExp () e
++                 ++ text ") "
++                 ++ self#pBlock () b)
++ 
++     | DoWhile (e, b, l) ->
++         self#pLineDirective l
++           ++ (align
++                 ++ text "do "
++                 ++ self#pBlock () b
++                 ++ text " while ("
++                 ++ self#pExp () e
++                 ++ text ");")
++ 
++     | For (bInit, e, bIter, b, l) ->
++ 	ignore (E.warn
++ 		  "in for loops, the 1st and 3rd expressions are not printed");
++           self#pLineDirective l
++             ++ (align
++                   ++ text "for ("
++                   ++ text "/* ??? */"   (* self#pBlock () bInit *)
++                   ++ text "; "
++                   ++ self#pExp () e
++                   ++ text "; "
++                   ++ text "/* ??? */"   (* self#pBlock() bIter *)
++                   ++ text ") "
++                   ++ self#pBlock () b)
++ 
+      | Block b -> align ++ self#pBlock () b
+        
+      | TryFinally (b, h, l) -> 
+***************
+*** 4705,4713 ****
+--- 4756,4781 ----
+      | Return (Some e, l) -> 
+          let e' = fExp e in
+          if e' != e then Return (Some e', l) else s.skind
++ (*
+      | Loop (b, l, s1, s2) -> 
+          let b' = fBlock b in
+          if b' != b then Loop (b', l, s1, s2) else s.skind
++ *)
++     | While (e, b, l) ->
++ 	let e' = fExp e in 
++         let b' = fBlock b in
++           if e' != e || b' != b then While (e', b', l) else s.skind
++     | DoWhile (e, b, l) ->
++ 	let b' = fBlock b in
++         let e' = fExp e in 
++           if e' != e || b' != b then DoWhile (e', b', l) else s.skind
++     | For (bInit, e, bIter, b, l) -> 
++ 	let bInit' = fBlock bInit in
++ 	let e' = fExp e in
++ 	let bIter' = fBlock bIter in
++ 	let b' = fBlock b in
++ 	  if bInit' != bInit || e' != e || bIter' != bIter || b' != b then
++ 	    For (bInit', e', bIter', b', l) else s.skind
+      | If(e, s1, s2, l) -> 
+          let e' = fExp e in 
+          (*if e queued any instructions, pop them here and remember them so that
+***************
+*** 5180,5186 ****
+--- 5248,5262 ----
+            peepHole1 doone tb.bstmts;
+            peepHole1 doone eb.bstmts
+        | Switch (e, b, _, _) -> peepHole1 doone b.bstmts
++ (*
+        | Loop (b, l, _, _) -> peepHole1 doone b.bstmts
++ *)
++       | While (_, b, _) -> peepHole1 doone b.bstmts
++       | DoWhile (_, b, _) -> peepHole1 doone b.bstmts
++       | For (bInit, _, bIter, b, _) ->
++ 	  peepHole1 doone bInit.bstmts;
++ 	  peepHole1 doone bIter.bstmts;
++ 	  peepHole1 doone b.bstmts
+        | Block b -> peepHole1 doone b.bstmts
+        | TryFinally (b, h, l) -> 
+            peepHole1 doone b.bstmts; 
+***************
+*** 5214,5220 ****
+--- 5290,5304 ----
+            peepHole2 dotwo tb.bstmts;
+            peepHole2 dotwo eb.bstmts
+        | Switch (e, b, _, _) -> peepHole2 dotwo b.bstmts
++ (*
+        | Loop (b, l, _, _) -> peepHole2 dotwo b.bstmts
++ *)
++       | While (_, b, _) -> peepHole2 dotwo b.bstmts
++       | DoWhile (_, b, _) -> peepHole2 dotwo b.bstmts
++       | For (bInit, _, bIter, b, _) ->
++ 	  peepHole2 dotwo bInit.bstmts;
++ 	  peepHole2 dotwo bIter.bstmts;
++ 	  peepHole2 dotwo b.bstmts
+        | Block b -> peepHole2 dotwo b.bstmts
+        | TryFinally (b, h, l) -> peepHole2 dotwo b.bstmts; 
+                                  peepHole2 dotwo h.bstmts
+***************
+*** 5887,5892 ****
+--- 5971,5977 ----
+          [] -> trylink s fallthrough
+        | hd :: tl -> (link s hd ; succpred_block b2 fallthrough ))
+  
++ (*
+    | Loop(b,l,_,_) -> 
+        begin match b.bstmts with
+          [] -> failwith "computeCFGInfo: empty loop" 
+***************
+*** 5894,5899 ****
+--- 5979,6011 ----
+            link s hd ; 
+            succpred_block b (Some(hd))
+        end
++ *)
++ 
++   | While (e, b, l) -> begin match b.bstmts with
++                        | [] -> failwith "computeCFGInfo: empty loop" 
++ 	               | hd :: tl -> link s hd ;
++                                      succpred_block b (Some(hd))
++                        end
++ 
++   | DoWhile (e, b, l) ->begin match b.bstmts with
++                        |  [] -> failwith "computeCFGInfo: empty loop" 
++ 	               | hd :: tl -> link s hd ;
++                                      succpred_block b (Some(hd))
++                        end
++ 
++   | For (bInit, e, bIter, b, l) ->
++       (match bInit.bstmts with
++          |  [] -> failwith "computeCFGInfo: empty loop" 
++ 	 | hd :: tl -> link s hd ;
++              succpred_block bInit (Some(hd))) ;
++       (match bIter.bstmts with
++          |  [] -> failwith "computeCFGInfo: empty loop" 
++ 	 | hd :: tl -> link s hd ;
++              succpred_block bIter (Some(hd))) ;
++       (match b.bstmts with
++          |  [] -> failwith "computeCFGInfo: empty loop" 
++ 	 | hd :: tl -> link s hd ;
++              succpred_block b (Some(hd))) ;
+  
+    | Block(b) -> begin match b.bstmts with
+                    [] -> trylink s fallthrough
+***************
+*** 5985,5991 ****
+        let i = get_switch_count () in 
+        let break_stmt = mkStmt (Instr []) in
+        break_stmt.labels <- 
+! 				[Label((Printf.sprintf "switch_%d_break" i),l,false)] ;
+        let break_block = mkBlock [ break_stmt ] in
+        let body_block = b in 
+        let body_if_stmtkind = (If(zero,body_block,break_block,l)) in
+--- 6097,6103 ----
+        let i = get_switch_count () in 
+        let break_stmt = mkStmt (Instr []) in
+        break_stmt.labels <- 
+! 	[Label((Printf.sprintf "switch_%d_break" i),l,false)] ;
+        let break_block = mkBlock [ break_stmt ] in
+        let body_block = b in 
+        let body_if_stmtkind = (If(zero,body_block,break_block,l)) in
+***************
+*** 6026,6039 ****
+        s.skind <- handle_choices (List.sort compare_choices sl) ;
+        xform_switch_block b (fun () -> ref break_stmt) cont_dest i 
+      end
+    | Loop(b,l,_,_) -> 
+            let i = get_switch_count () in 
+            let break_stmt = mkStmt (Instr []) in
+            break_stmt.labels <- 
+! 						[Label((Printf.sprintf "while_%d_break" i),l,false)] ;
+            let cont_stmt = mkStmt (Instr []) in
+            cont_stmt.labels <- 
+! 						[Label((Printf.sprintf "while_%d_continue" i),l,false)] ;
+            b.bstmts <- cont_stmt :: b.bstmts ;
+            let this_stmt = mkStmt 
+              (Loop(b,l,Some(cont_stmt),Some(break_stmt))) in 
+--- 6138,6152 ----
+        s.skind <- handle_choices (List.sort compare_choices sl) ;
+        xform_switch_block b (fun () -> ref break_stmt) cont_dest i 
+      end
++ (*
+    | Loop(b,l,_,_) -> 
+            let i = get_switch_count () in 
+            let break_stmt = mkStmt (Instr []) in
+            break_stmt.labels <- 
+! 	    [Label((Printf.sprintf "while_%d_break" i),l,false)] ;
+            let cont_stmt = mkStmt (Instr []) in
+            cont_stmt.labels <- 
+! 	    [Label((Printf.sprintf "while_%d_continue" i),l,false)] ;
+            b.bstmts <- cont_stmt :: b.bstmts ;
+            let this_stmt = mkStmt 
+              (Loop(b,l,Some(cont_stmt),Some(break_stmt))) in 
+***************
+*** 6043,6048 ****
+--- 6156,6217 ----
+            break_stmt.succs <- s.succs ; 
+            let new_block = mkBlock [ this_stmt ; break_stmt ] in
+            s.skind <- Block new_block
++ *)
++   | While (e, b, l) ->
++           let i = get_switch_count () in 
++           let break_stmt = mkStmt (Instr []) in
++           break_stmt.labels <- 
++ 	    [Label((Printf.sprintf "while_%d_break" i),l,false)] ;
++           let cont_stmt = mkStmt (Instr []) in
++           cont_stmt.labels <- 
++ 	    [Label((Printf.sprintf "while_%d_continue" i),l,false)] ;
++           b.bstmts <- cont_stmt :: b.bstmts ;
++           let this_stmt = mkStmt 
++             (While(e,b,l)) in 
++           let break_dest () = ref break_stmt in
++           let cont_dest () = ref cont_stmt in 
++           xform_switch_block b break_dest cont_dest label_index ;
++           break_stmt.succs <- s.succs ; 
++           let new_block = mkBlock [ this_stmt ; break_stmt ] in
++           s.skind <- Block new_block
++ 
++   | DoWhile (e, b, l) ->
++           let i = get_switch_count () in 
++           let break_stmt = mkStmt (Instr []) in
++           break_stmt.labels <- 
++ 	    [Label((Printf.sprintf "while_%d_break" i),l,false)] ;
++           let cont_stmt = mkStmt (Instr []) in
++           cont_stmt.labels <- 
++ 	    [Label((Printf.sprintf "while_%d_continue" i),l,false)] ;
++           b.bstmts <- cont_stmt :: b.bstmts ;
++           let this_stmt = mkStmt 
++             (DoWhile(e,b,l)) in 
++           let break_dest () = ref break_stmt in
++           let cont_dest () = ref cont_stmt in 
++           xform_switch_block b break_dest cont_dest label_index ;
++           break_stmt.succs <- s.succs ; 
++           let new_block = mkBlock [ this_stmt ; break_stmt ] in
++           s.skind <- Block new_block
++ 
++   | For (bInit, e, bIter , b, l) ->
++           let i = get_switch_count () in 
++           let break_stmt = mkStmt (Instr []) in
++           break_stmt.labels <- 
++ 	    [Label((Printf.sprintf "while_%d_break" i),l,false)] ;
++           let cont_stmt = mkStmt (Instr []) in
++           cont_stmt.labels <- 
++ 	    [Label((Printf.sprintf "while_%d_continue" i),l,false)] ;
++           b.bstmts <- cont_stmt :: b.bstmts ;
++           let this_stmt = mkStmt 
++             (For(bInit,e,bIter,b,l)) in 
++           let break_dest () = ref break_stmt in
++           let cont_dest () = ref cont_stmt in 
++           xform_switch_block b break_dest cont_dest label_index ;
++           break_stmt.succs <- s.succs ; 
++           let new_block = mkBlock [ this_stmt ; break_stmt ] in
++           s.skind <- Block new_block
++ 
++ 
+    | Block(b) -> xform_switch_block b break_dest cont_dest label_index
+  
+    | TryExcept _ | TryFinally _ ->