Commit a5f03d96 authored by xleroy's avatar xleroy
Browse files

Cleaned up configure script.

Distribution of CIL as an expanded source tree with changes applied
(instead of original .tar.gz + patches to be applied at config time).


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent a9621943
......@@ -37,14 +37,12 @@ files are free software and can be used both in commercial and
non-commercial contexts, subject to the terms of the GNU General
Public License.
This distribution includes a copy of the CIL library and modifications
to this library in the form of patches. The CIL library is Copyright
2001-2005 George C. Necula, Scott McPeak, Wes Weimer and Ben Liblit.
The modifications contained in the sub-directory cil.patches/ of this
distribution are Copyright 2006, 2007, 2008, 2009 Institut National de
Recherche en Informatique et en Automatique. The CIL library and the
modifications contained in the sub-directory cil.patches/ are
distributed under the terms of the BSD license, included below.
This distribution includes a modified copy of the CIL library.
The CIL library is Copyright 2001-2005 George C. Necula, Scott McPeak,
Wes Weimer and Ben Liblit. The modifications are Copyright 2006,
2007, 2008, 2009 Institut National de Recherche en Informatique et en
Automatique. The CIL library and the modifications are distributed
under the terms of the BSD license, included below.
----------------------------------------------------------------------
......
--- ../cil/Makefile.in.orig 2008-12-31 19:08:43.000000000 +0100
+++ ../cil/Makefile.in 2008-12-31 19:09:00.000000000 +0100
@@ -212,7 +212,7 @@
# build two libraries
.PHONY: cillib libcil
ifeq ($(NATIVECAML),1)
-cillib: $(OBJDIR)/cil.$(CMXA) $(OBJDIR)/libcil.a
+cillib: $(OBJDIR)/cil.$(CMXA) # $(OBJDIR)/libcil.a
else
cillib: $(OBJDIR)/cil.$(CMXA)
endif
@@ -243,9 +243,9 @@
echo " Zrapp.feature;" >> $@
endif
# Now the extra features, with the first letter capitalized
- echo -ne \
+ echo \
$(foreach f,@EXTRAFEATURES@, \
- `echo $f | cut -c 1 | tr "[a-z]" "[A-Z]"``echo $f | cut -c 2-`".feature;\n") >> $@
+ `echo $f | cut -c 1 | tr "[a-z]" "[A-Z]"``echo $f | cut -c 2-`".feature;") >> $@
echo "]" >>$@
# Must delete main.d and remake it, because it may have been made
# before feature_config existed.
*** ../cil/src/ext/astslicer.ml 2006-05-21 06:14:15.000000000 +0200
--- ../cil_patch/src/ext/astslicer.ml 2006-06-20 17:24:22.000000000 +0200
***************
*** 1,3 ****
--- 1,5 ----
+ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
+
(*
*
* Copyright (c) 2001-2002,
***************
*** 97,103 ****
--- 99,110 ----
Printf.fprintf out ")\n" ;
incr i
| Switch(_,b,_,_)
+ (*
| Loop(b,_,_,_)
+ *)
+ | While(_,b,_)
+ | DoWhile(_,b,_)
+ | For(_,_,_,b,_)
| Block(b) ->
emit base i st_ht s ;
decr i ;
***************
*** 371,377 ****
--- 378,389 ----
doBlock b2 base'' i'' inside ;
incr i
| Switch(_,b,_,_)
+ (*
| Loop(b,_,_,_)
+ *)
+ | While(_,b,_)
+ | DoWhile(_,b,_)
+ | For(_,_,_,b,_)
| Block(b) ->
let inside = check base i default in
mark ws s inside ;
*** ../cil.orig/src/frontc/cabs2cil.ml 2006-05-21 06:14:15.000000000 +0200
--- ../cil/src/frontc/cabs2cil.ml 2008-04-19 10:17:27.000000000 +0200
***************
*** 1,3 ****
--- 1,11 ----
+ (* MODIF: allow E.Error to propagate *)
+
+ (* MODIF: for pointer comparison, avoid systematic cast to unsigned int *)
+
+ (* 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 *)
--- 824,839 ----
(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 ****
--- 849,855 ----
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 ****
--- 857,889 ----
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 ****
--- 998,1004 ----
(************ 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 ****
--- 1011,1041 ----
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
+ | ContinueUnchanged
+
+ 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
+ | ContinueUnchanged :: _ -> 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 ****
--- 1051,1057 ----
[] -> 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
***************
*** 4141,4151 ****
| _ -> E.s (error "%a operator on a non-integer type" d_binop bop)
in
let pointerComparison e1 t1 e2 t2 =
! (* Cast both sides to an integer *)
! let commontype = !upointType in
intType,
! optConstFoldBinOp false bop (mkCastT e1 t1 commontype)
! (mkCastT e2 t2 commontype) intType
in
match bop with
--- 4203,4211 ----
| _ -> E.s (error "%a operator on a non-integer type" d_binop bop)
in
let pointerComparison e1 t1 e2 t2 =
! (* XL: Do not cast both sides -- what's the point? *)
intType,
! optConstFoldBinOp false bop e1 e2 intType
in
match bop with
***************
*** 4194,4207 ****
| (Eq|Ne|Le|Lt|Ge|Gt) when isPointerType t1 && isArithmeticType t2 ->
ignore (warnOpt "Comparison of pointer and non-pointer");
! (* Cast both values to upointType *)
! doBinOp bop (mkCastT e1 t1 !upointType) !upointType
! (mkCastT e2 t2 !upointType) !upointType
| (Eq|Ne|Le|Lt|Ge|Gt) when isArithmeticType t1 && isPointerType t2 ->
ignore (warnOpt "Comparison of pointer and non-pointer");
! (* Cast both values to upointType *)
! doBinOp bop (mkCastT e1 t1 !upointType) !upointType
! (mkCastT e2 t2 !upointType) !upointType
| _ -> E.s (error "doBinOp: %a\n" d_plainexp (BinOp(bop,e1,e2,intType)))
--- 4254,4267 ----
| (Eq|Ne|Le|Lt|Ge|Gt) when isPointerType t1 && isArithmeticType t2 ->
ignore (warnOpt "Comparison of pointer and non-pointer");
! (* Cast both values to void * *)
! doBinOp bop (mkCastT e1 t1 voidPtrType) voidPtrType
! (mkCastT e2 t2 voidPtrType) voidPtrType
| (Eq|Ne|Le|Lt|Ge|Gt) when isArithmeticType t1 && isPointerType t2 ->
ignore (warnOpt "Comparison of pointer and non-pointer");
! (* Cast both values to void * *)
! doBinOp bop (mkCastT e1 t1 voidPtrType) voidPtrType
! (mkCastT e2 t2 voidPtrType) voidPtrType
| _ -> E.s (error "doBinOp: %a\n" d_plainexp (BinOp(bop,e1,e2,intType)))
***************
*** 5465,5473 ****
--- 5525,5538 ----
* 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
--- 5577,5583 ----
| 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 ****
--- 5587,5593 ----
List.exists stmtCanBreak b.bstmts
in
if blockFallsThrough !currentFunctionFDEC.sbody then begin
+ (*
let retval =
match unrollType !currentReturnType with
TVoid _ -> None
***************
*** 5537,5549 ****
!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"
n docEnv); *)
cabsPushGlobal (GFun (!currentFunctionFDEC, funloc));
empty
! with e -> begin
ignore (E.log "error in collectFunction %s: %s\n"
n (Printexc.to_string e));
cabsPushGlobal (GAsm("error in function " ^ n, !currentLoc));
--- 5603,5617 ----
!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"
n docEnv); *)
cabsPushGlobal (GFun (!currentFunctionFDEC, funloc));
empty
! with E.Error as e -> raise e
! | e -> begin
ignore (E.log "error in collectFunction %s: %s\n"
n (Printexc.to_string e));
cabsPushGlobal (GAsm("error in function " ^ n, !currentLoc));
***************
*** 5596,5609 ****
* local context *)
addLocalToEnv (kindPlusName "type" n) (EnvTyp namedTyp);
cabsPushGlobal (GType (ti, !currentLoc))
! with e -> begin
ignore (E.log "Error on A.TYPEDEF (%s)\n"
(Printexc.to_string e));
cabsPushGlobal (GAsm ("booo_typedef:" ^ n, !currentLoc))
end
in
List.iter createTypedef nl
! with e -> begin
ignore (E.log "Error on A.TYPEDEF (%s)\n"
(Printexc.to_string e));
let fstname =
--- 5664,5679 ----
* local context *)
addLocalToEnv (kindPlusName "type" n) (EnvTyp namedTyp);
cabsPushGlobal (GType (ti, !currentLoc))
! with E.Error as e -> raise e
! | e -> begin
ignore (E.log "Error on A.TYPEDEF (%s)\n"
(Printexc.to_string e));
cabsPushGlobal (GAsm ("booo_typedef:" ^ n, !currentLoc))
end
in
List.iter createTypedef nl
! with E.Error as e -> raise e
! | e -> begin
ignore (E.log "Error on A.TYPEDEF (%s)\n"
(Printexc.to_string e));
let fstname =
***************
*** 5650,5656 ****
| _ ->
ignore (warn "Ignoring un-named typedef that does not introduce a struct or enumeration type\n")
! with e -> begin
ignore (E.log "Error on A.ONLYTYPEDEF (%s)\n"
(Printexc.to_string e));
cabsPushGlobal (GAsm ("booo_typedef", !currentLoc))
--- 5720,5727 ----
| _ ->
ignore (warn "Ignoring un-named typedef that does not introduce a struct or enumeration type\n")
! with E.Error as e -> raise e
! | e -> begin
ignore (E.log "Error on A.ONLYTYPEDEF (%s)\n"
(Printexc.to_string e));
cabsPushGlobal (GAsm ("booo_typedef", !currentLoc))
***************
*** 5738,5743 ****
--- 5809,5815 ----
doCondition false e st' sf'
| A.WHILE(e,s,loc) ->
+ (*
startLoop true;
let s' = doStatement s in
exitLoop ();
***************
*** 5746,5753 ****
--- 5818,5844 ----
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 *)
--- 5848,5874 ----
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 ****
--- 5894,5928 ----
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; bCond}, {doStatement(s)})
+ where doStatement(A.CONTINUE) = Cil.Continue. *)
+
+ startLoop ContinueUnchanged;
+ let s' = doStatement s in
+ exitLoop ();
+ let loc' = convLoc loc in
+ currentLoc := loc';
+ (forChunk (bInit @@ bCond) eCond' (bIter @@ bCond) s')
+
| A.BREAK loc ->
let loc' = convLoc loc in
currentLoc := loc';
***************
*** 5792,5798 ****
--- 5931,5940 ----
| A.CONTINUE loc ->
let loc' = convLoc loc in
currentLoc := loc';
+ (*
continueOrLabelChunk loc'
+ *)
+ continueDuplicateChunk loc'
| A.RETURN (A.NOTHING, loc) ->
let loc' = convLoc loc in
*** ../cil/src/ext/cfg.ml 2006-05-21 06:14:15.000000000 +0200
--- ../cil_patch/src/ext/cfg.ml 2006-06-20 17:42:04.000000000 +0200
***************
*** 1,3 ****
--- 1,5 ----
+ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
+
(*
*
* Copyright (c) 2001-2003,
***************
*** 156,162 ****
--- 158,169 ----
then
addOptionSucc next;
cfgBlock blk next next cont
+ (*
| Loop(blk,_,_,_) ->
+ *)
+ | While(_,blk,_)
+ | DoWhile(_,blk,_)
+ | For(_,_,_,blk,_) ->
addBlockSucc blk;
cfgBlock blk (Some s) next (Some s)
(* Since all loops have terminating condition true, we don't put
***************
*** 184,190 ****
--- 191,202 ----
| Block b -> fasBlock todo b
| If (_, tb, fb, _) -> (fasBlock todo tb; fasBlock todo fb)
| Switch (_, b, _, _) -> fasBlock todo b
+ (*
| Loop (b, _, _, _) -> fasBlock todo b
+ *)
+ | While (_, b, _) -> fasBlock todo b
+ | DoWhile (_, b, _) -> fasBlock todo b
+ | For (_, _, _, b, _) -> fasBlock todo b
| (Return _ | Break _ | Continue _ | Goto _ | Instr _) -> ()
| TryExcept _ | TryFinally _ -> E.s (E.unimp "try/except/finally")
end
***************
*** 201,207 ****
--- 213,224 ----
begin
match s.skind with
| If (e, _, _, _) -> "if" (*sprint ~width:999 (dprintf "if %a" d_exp e)*)
+ (*
| Loop _ -> "loop"
+ *)
+ | While _ -> "while"
+ | DoWhile _ -> "dowhile"
+ | For _ -> "for"
| Break _ -> "break"
| Continue _ -> "continue"
| Goto _ -> "goto"
*** ../cil/src/check.ml 2006-05-21 06:14:15.000000000 +0200
--- ../cil_patch/src/check.ml 2006-06-21 11:13:35.000000000 +0200
***************
*** 1,3 ****
--- 1,5 ----
+ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
+
(*
*
* Copyright (c) 2001-2002,
***************
*** 661,667 ****
(fun _ ->
(* Print context only for certain small statements *)
match s.skind with
! Loop _ | If _ | Switch _ -> nil
| _ -> dprintf "checkStmt: %a" d_stmt s)
(fun _ ->
(* Check the labels *)
--- 663,669 ----
(fun _ ->
(* Print context only for certain small statements *)
match s.skind with
! (*Loop _*) While _ | DoWhile _ | For _ | If _ | Switch _ -> nil
| _ -> dprintf "checkStmt: %a" d_stmt s)
(fun _ ->
(* Check the labels *)
***************
*** 704,710 ****
--- 706,731 ----
| None, _ -> ignore (warn "Invalid return value")
| Some re', rt' -> checkExpType false re' rt'
end
+ (*
| Loop (b, l, _, _) -> checkBlock b
+ *)
+ | While (e, b, l) ->
+ currentLoc := l;
+ let te = checkExp false e in
+ checkBooleanType te;
+ checkBlock b;
+ | DoWhile (e, b, l) ->
+ currentLoc := l;
<