From 48c970f12e3d993f56f51103df134a4a6847e6ad Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 24 Oct 2022 17:49:23 +0200 Subject: [PATCH 01/15] add test cases --- README.md | 4 ++ src/ciloptions.ml | 48 +++++++++++++----------- src/cilutil.ml | 6 ++- src/mergecil.ml | 2 +- test/Makefile | 9 ++++- test/small1/combine-c99-mergeinline1_1.c | 3 ++ test/small1/combine-c99-mergeinline1_2.c | 7 ++++ test/small1/combine-c99-mergeinline2_1.c | 3 ++ test/small1/combine-c99-mergeinline2_2.c | 7 ++++ test/small1/combine-c99-mergeinline3_1.c | 3 ++ test/small1/combine-c99-mergeinline3_2.c | 7 ++++ test/small1/combine-c99-mergeinline4_1.c | 3 ++ test/small1/combine-c99-mergeinline4_2.c | 7 ++++ test/small1/combine-c99-mergeinline5_1.c | 3 ++ test/small1/combine-c99-mergeinline5_2.c | 7 ++++ test/small1/combine-c99-mergeinline6_1.c | 3 ++ test/small1/combine-c99-mergeinline6_2.c | 7 ++++ test/small1/combine-c99inline1_1.c | 3 ++ test/small1/combine-c99inline1_2.c | 7 ++++ test/small1/combine-c99inline2_1.c | 3 ++ test/small1/combine-c99inline2_2.c | 7 ++++ test/small1/combine-c99inline3_1.c | 3 ++ test/small1/combine-c99inline3_2.c | 7 ++++ test/small1/combine-c99inline4_1.c | 3 ++ test/small1/combine-c99inline4_2.c | 7 ++++ test/small1/combine-c99inline5_1.c | 3 ++ test/small1/combine-c99inline5_2.c | 7 ++++ test/small1/combine-c99inline6_1.c | 3 ++ test/small1/combine-c99inline6_2.c | 7 ++++ 29 files changed, 164 insertions(+), 25 deletions(-) create mode 100644 test/small1/combine-c99-mergeinline1_1.c create mode 100644 test/small1/combine-c99-mergeinline1_2.c create mode 100644 test/small1/combine-c99-mergeinline2_1.c create mode 100644 test/small1/combine-c99-mergeinline2_2.c create mode 100644 test/small1/combine-c99-mergeinline3_1.c create mode 100644 test/small1/combine-c99-mergeinline3_2.c create mode 100644 test/small1/combine-c99-mergeinline4_1.c create mode 100644 test/small1/combine-c99-mergeinline4_2.c create mode 100644 test/small1/combine-c99-mergeinline5_1.c create mode 100644 test/small1/combine-c99-mergeinline5_2.c create mode 100644 test/small1/combine-c99-mergeinline6_1.c create mode 100644 test/small1/combine-c99-mergeinline6_2.c create mode 100644 test/small1/combine-c99inline1_1.c create mode 100644 test/small1/combine-c99inline1_2.c create mode 100644 test/small1/combine-c99inline2_1.c create mode 100644 test/small1/combine-c99inline2_2.c create mode 100644 test/small1/combine-c99inline3_1.c create mode 100644 test/small1/combine-c99inline3_2.c create mode 100644 test/small1/combine-c99inline4_1.c create mode 100644 test/small1/combine-c99inline4_2.c create mode 100644 test/small1/combine-c99inline5_1.c create mode 100644 test/small1/combine-c99inline5_2.c create mode 100644 test/small1/combine-c99inline6_1.c create mode 100644 test/small1/combine-c99inline6_2.c diff --git a/README.md b/README.md index 27be957ac..befe59c7e 100644 --- a/README.md +++ b/README.md @@ -52,6 +52,10 @@ commands to build and test `goblint-cil`: dune build dune runtest # runs the regression test suite +To run a single test go to the build directory (e.g. `_build/default/test`) and run e.g.: + + dune exec -- make test/array1 + You can also install `goblint-cil` into the opam switch: dune build @install diff --git a/src/ciloptions.ml b/src/ciloptions.ml index d9f1ce667..178822940 100644 --- a/src/ciloptions.ml +++ b/src/ciloptions.ml @@ -6,7 +6,7 @@ Wes Weimer Ben Liblit All rights reserved. - + Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: @@ -39,16 +39,16 @@ open GoblintCil module E = Errormsg -let setDebugFlag v name = +let setDebugFlag v name = E.debugFlag := v; if v then Pretty.flushOften := true -type outfile = +type outfile = { fname: string; - fchan: out_channel } + fchan: out_channel } (* Processign of output file arguments *) -let openFile (what: string) (takeit: outfile -> unit) (fl: string) = +let openFile (what: string) (takeit: outfile -> unit) (fl: string) = if !E.verboseFlag then ignore (Printf.printf "Setting %s to %s\n" what fl); (try takeit { fname = fl; @@ -58,44 +58,44 @@ let openFile (what: string) (takeit: outfile -> unit) (fl: string) = let fileNames : string list ref = ref [] -let recordFile fname = - fileNames := fname :: (!fileNames) +let recordFile fname = + fileNames := fname :: (!fileNames) (* Parsing of files with additional names *) -let parseExtraFile (s: string) = +let parseExtraFile (s: string) = try let sfile = open_in s in while true do let line = try input_line sfile with e -> (close_in sfile; raise e) in let linelen = String.length line in let rec scan (pos: int) (* next char to look at *) - (start: int) : unit (* start of the word, + (start: int) : unit (* start of the word, or -1 if none *) = - if pos >= linelen then - if start >= 0 then + if pos >= linelen then + if start >= 0 then recordFile (String.sub line start (pos - start)) - else + else () (* Just move on to the next line *) else let c = String.get line pos in - match c with - ' ' | '\n' | '\r' | '\t' -> + match c with + ' ' | '\n' | '\r' | '\t' -> (* whitespace *) if start >= 0 then begin recordFile (String.sub line start (pos - start)); end; scan (pos + 1) (-1) - + | _ -> (* non-whitespace *) - if start >= 0 then - scan (pos + 1) start + if start >= 0 then + scan (pos + 1) start else scan (pos + 1) pos in scan 0 (-1) done with Sys_error _ -> E.s (E.error "Cannot find extra file: %s" s) - | End_of_file -> () + | End_of_file -> () let options : (string * Arg.spec * string) list = @@ -130,7 +130,7 @@ let options : (string * Arg.spec * string) list = Arg.Clear E.warnFlag, (" Disable optional warnings" ^ is_default (not !E.warnFlag)); - "--noTruncateWarning", + "--noTruncateWarning", Arg.Clear Cil.warnTruncate, " Suppress warning about truncating integer constants"; @@ -167,6 +167,12 @@ let options : (string * Arg.spec * string) list = " Same as --check, but treats problems as errors not warnings."; "", Arg.Unit (fun _ -> ()), ""; + "--mergeinlines", Arg.Unit (fun _ -> Cilutil.merge_inlines := true), + " Try to merge definitions of inline functions. They can appear in multiple + files and we would like them all to be the same. This can slow down the + merger an order of magnitude."; + "", Arg.Unit (fun _ -> ()), ""; + "--noPrintLn", Arg.Unit (fun _ -> Cil.lineDirectiveStyle := None; @@ -179,7 +185,7 @@ let options : (string * Arg.spec * string) list = Cprint.printLnComment := true), " Print #line directives in the output, but put them in comments"; - "--commPrintLnSparse", + "--commPrintLnSparse", Arg.Unit (fun _ -> Cil.lineDirectiveStyle := Some Cil.LineCommentSparse; Cprint.printLnComment := true), @@ -204,7 +210,7 @@ let options : (string * Arg.spec * string) list = try let machineModel = Sys.getenv "CIL_MACHINE" in Cil.envMachine := Some (Machdepenv.modelParse machineModel); - with + with Not_found -> ignore (E.error "CIL_MACHINE environment variable is not set") | Failure msg -> diff --git a/src/cilutil.ml b/src/cilutil.ml index 79ab1cc67..b8bd102b1 100644 --- a/src/cilutil.ml +++ b/src/cilutil.ml @@ -1,11 +1,11 @@ (* - Copyright (c) 2001-2002, + Copyright (c) 2001-2002, George C. Necula Scott McPeak Wes Weimer All rights reserved. - + Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: @@ -49,3 +49,5 @@ let sliceGlobal = ref false let printStages = ref false + +let merge_inlines = ref false diff --git a/src/mergecil.ml b/src/mergecil.ml index 89b3b6698..f9e17d0e9 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -62,7 +62,7 @@ (* Try to merge definitions of inline functions. They can appear in multiple files and we would like them all to be the same. This can slow down the merger an order of magnitude !!! *) - let merge_inlines = ref false + let merge_inlines = Cilutil.merge_inlines let mergeInlinesRepeat () = !merge_inlines && true let mergeInlinesWithAlphaConvert () = !merge_inlines && true diff --git a/test/Makefile b/test/Makefile index 60384da59..914c860f9 100644 --- a/test/Makefile +++ b/test/Makefile @@ -304,11 +304,18 @@ arcombine: mustbegcc combinec99%: $(SMALL1)/combine-c99%_1.c cd $(SMALL1); \ - $(CILLY) $(CFLAGS) -std=c99 -fcommon --merge \ + $(CILLY) $(CFLAGS) -O1 -std=c99 --verbose -fcommon --merge \ $(notdir $(wildcard $(SMALL1)/combine-c99$*_[1-9].c)) \ $(EXEOUT)combine-c99$*.exe cd $(SMALL1); ./combine-c99$*.exe +combinec99mergeinline%: $(SMALL1)/combine-c99-mergeinline%_1.c + cd $(SMALL1); \ + $(CILLY) $(CFLAGS) -O1 -std=c99 --verbose -fcommon --merge --mergeinlines \ + $(notdir $(wildcard $(SMALL1)/combine-c99-mergeinline$*_[1-9].c)) \ + $(EXEOUT)combine-c99-mergeinline$*.exe + cd $(SMALL1); ./combine-c99-mergeinline$*.exe + # ww: Scott's structs-edg-stl.c example structs : mustbemanju cd /usr/src/big-examples/; $(CILLY) --nomerge \ diff --git a/test/small1/combine-c99-mergeinline1_1.c b/test/small1/combine-c99-mergeinline1_1.c new file mode 100644 index 000000000..d723ea774 --- /dev/null +++ b/test/small1/combine-c99-mergeinline1_1.c @@ -0,0 +1,3 @@ +int add(int i, int j) { + return i + j; +} diff --git a/test/small1/combine-c99-mergeinline1_2.c b/test/small1/combine-c99-mergeinline1_2.c new file mode 100644 index 000000000..ef3178329 --- /dev/null +++ b/test/small1/combine-c99-mergeinline1_2.c @@ -0,0 +1,7 @@ +inline int add(int i, int j) { + return i + j; +} + +int main() { + return add(-3, 3); +} diff --git a/test/small1/combine-c99-mergeinline2_1.c b/test/small1/combine-c99-mergeinline2_1.c new file mode 100644 index 000000000..5b5f19aaa --- /dev/null +++ b/test/small1/combine-c99-mergeinline2_1.c @@ -0,0 +1,3 @@ +inline int add(int i, int j) { + return i + j; +} diff --git a/test/small1/combine-c99-mergeinline2_2.c b/test/small1/combine-c99-mergeinline2_2.c new file mode 100644 index 000000000..ef3178329 --- /dev/null +++ b/test/small1/combine-c99-mergeinline2_2.c @@ -0,0 +1,7 @@ +inline int add(int i, int j) { + return i + j; +} + +int main() { + return add(-3, 3); +} diff --git a/test/small1/combine-c99-mergeinline3_1.c b/test/small1/combine-c99-mergeinline3_1.c new file mode 100644 index 000000000..5b5f19aaa --- /dev/null +++ b/test/small1/combine-c99-mergeinline3_1.c @@ -0,0 +1,3 @@ +inline int add(int i, int j) { + return i + j; +} diff --git a/test/small1/combine-c99-mergeinline3_2.c b/test/small1/combine-c99-mergeinline3_2.c new file mode 100644 index 000000000..a2ba360da --- /dev/null +++ b/test/small1/combine-c99-mergeinline3_2.c @@ -0,0 +1,7 @@ +int add(int i, int j) { + return i + j; +} + +int main() { + return add(-3, 3); +} diff --git a/test/small1/combine-c99-mergeinline4_1.c b/test/small1/combine-c99-mergeinline4_1.c new file mode 100644 index 000000000..b59be1ca6 --- /dev/null +++ b/test/small1/combine-c99-mergeinline4_1.c @@ -0,0 +1,3 @@ +int add(int i, int j) { + return i - j; +} diff --git a/test/small1/combine-c99-mergeinline4_2.c b/test/small1/combine-c99-mergeinline4_2.c new file mode 100644 index 000000000..ef3178329 --- /dev/null +++ b/test/small1/combine-c99-mergeinline4_2.c @@ -0,0 +1,7 @@ +inline int add(int i, int j) { + return i + j; +} + +int main() { + return add(-3, 3); +} diff --git a/test/small1/combine-c99-mergeinline5_1.c b/test/small1/combine-c99-mergeinline5_1.c new file mode 100644 index 000000000..218ab7327 --- /dev/null +++ b/test/small1/combine-c99-mergeinline5_1.c @@ -0,0 +1,3 @@ +inline int add(int i, int j) { + return i - j; +} diff --git a/test/small1/combine-c99-mergeinline5_2.c b/test/small1/combine-c99-mergeinline5_2.c new file mode 100644 index 000000000..ef3178329 --- /dev/null +++ b/test/small1/combine-c99-mergeinline5_2.c @@ -0,0 +1,7 @@ +inline int add(int i, int j) { + return i + j; +} + +int main() { + return add(-3, 3); +} diff --git a/test/small1/combine-c99-mergeinline6_1.c b/test/small1/combine-c99-mergeinline6_1.c new file mode 100644 index 000000000..218ab7327 --- /dev/null +++ b/test/small1/combine-c99-mergeinline6_1.c @@ -0,0 +1,3 @@ +inline int add(int i, int j) { + return i - j; +} diff --git a/test/small1/combine-c99-mergeinline6_2.c b/test/small1/combine-c99-mergeinline6_2.c new file mode 100644 index 000000000..a2ba360da --- /dev/null +++ b/test/small1/combine-c99-mergeinline6_2.c @@ -0,0 +1,7 @@ +int add(int i, int j) { + return i + j; +} + +int main() { + return add(-3, 3); +} diff --git a/test/small1/combine-c99inline1_1.c b/test/small1/combine-c99inline1_1.c new file mode 100644 index 000000000..d723ea774 --- /dev/null +++ b/test/small1/combine-c99inline1_1.c @@ -0,0 +1,3 @@ +int add(int i, int j) { + return i + j; +} diff --git a/test/small1/combine-c99inline1_2.c b/test/small1/combine-c99inline1_2.c new file mode 100644 index 000000000..c5b5ec4bf --- /dev/null +++ b/test/small1/combine-c99inline1_2.c @@ -0,0 +1,7 @@ +inline int add(int i, int j) { + return i + j; +} + +int main() { + return add(3, -3); +} diff --git a/test/small1/combine-c99inline2_1.c b/test/small1/combine-c99inline2_1.c new file mode 100644 index 000000000..5b5f19aaa --- /dev/null +++ b/test/small1/combine-c99inline2_1.c @@ -0,0 +1,3 @@ +inline int add(int i, int j) { + return i + j; +} diff --git a/test/small1/combine-c99inline2_2.c b/test/small1/combine-c99inline2_2.c new file mode 100644 index 000000000..c5b5ec4bf --- /dev/null +++ b/test/small1/combine-c99inline2_2.c @@ -0,0 +1,7 @@ +inline int add(int i, int j) { + return i + j; +} + +int main() { + return add(3, -3); +} diff --git a/test/small1/combine-c99inline3_1.c b/test/small1/combine-c99inline3_1.c new file mode 100644 index 000000000..5b5f19aaa --- /dev/null +++ b/test/small1/combine-c99inline3_1.c @@ -0,0 +1,3 @@ +inline int add(int i, int j) { + return i + j; +} diff --git a/test/small1/combine-c99inline3_2.c b/test/small1/combine-c99inline3_2.c new file mode 100644 index 000000000..a2ba360da --- /dev/null +++ b/test/small1/combine-c99inline3_2.c @@ -0,0 +1,7 @@ +int add(int i, int j) { + return i + j; +} + +int main() { + return add(-3, 3); +} diff --git a/test/small1/combine-c99inline4_1.c b/test/small1/combine-c99inline4_1.c new file mode 100644 index 000000000..b59be1ca6 --- /dev/null +++ b/test/small1/combine-c99inline4_1.c @@ -0,0 +1,3 @@ +int add(int i, int j) { + return i - j; +} diff --git a/test/small1/combine-c99inline4_2.c b/test/small1/combine-c99inline4_2.c new file mode 100644 index 000000000..ef3178329 --- /dev/null +++ b/test/small1/combine-c99inline4_2.c @@ -0,0 +1,7 @@ +inline int add(int i, int j) { + return i + j; +} + +int main() { + return add(-3, 3); +} diff --git a/test/small1/combine-c99inline5_1.c b/test/small1/combine-c99inline5_1.c new file mode 100644 index 000000000..218ab7327 --- /dev/null +++ b/test/small1/combine-c99inline5_1.c @@ -0,0 +1,3 @@ +inline int add(int i, int j) { + return i - j; +} diff --git a/test/small1/combine-c99inline5_2.c b/test/small1/combine-c99inline5_2.c new file mode 100644 index 000000000..ef3178329 --- /dev/null +++ b/test/small1/combine-c99inline5_2.c @@ -0,0 +1,7 @@ +inline int add(int i, int j) { + return i + j; +} + +int main() { + return add(-3, 3); +} diff --git a/test/small1/combine-c99inline6_1.c b/test/small1/combine-c99inline6_1.c new file mode 100644 index 000000000..218ab7327 --- /dev/null +++ b/test/small1/combine-c99inline6_1.c @@ -0,0 +1,3 @@ +inline int add(int i, int j) { + return i - j; +} diff --git a/test/small1/combine-c99inline6_2.c b/test/small1/combine-c99inline6_2.c new file mode 100644 index 000000000..a2ba360da --- /dev/null +++ b/test/small1/combine-c99inline6_2.c @@ -0,0 +1,7 @@ +int add(int i, int j) { + return i + j; +} + +int main() { + return add(-3, 3); +} From 6d4cae2623e1eb8e589e8f07f8b14c352d9c8ada Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Tue, 8 Nov 2022 11:19:20 +0100 Subject: [PATCH 02/15] implement c99 inline semantic --- src/mergecil.ml | 20 +++++++++----------- test/testcil.pl | 12 ++++++++++++ 2 files changed, 21 insertions(+), 11 deletions(-) diff --git a/src/mergecil.ml b/src/mergecil.ml index f9e17d0e9..67465b634 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -809,7 +809,7 @@ then newrep.ndata.vtype <- typeRemoveAttributes [ "const"; "pconst" ] newtype else newrep.ndata.vtype <- newtype; - (* clean up the storage. *) + (* clean up the storage. *) let newstorage = if vi.vstorage = oldvi.vstorage || vi.vstorage = Extern then oldvi.vstorage @@ -841,7 +841,7 @@ currentLoc := l; incr currentDeclIdx; vi.vreferenced <- false; - if vi.vstorage <> Static then matchVarinfo vi (l, !currentDeclIdx) + if vi.vstorage <> Static && (not vi.vinline || vi.vstorage = Extern) then matchVarinfo vi (l, !currentDeclIdx) | GFun (fdec, l) -> currentLoc := l; incr currentDeclIdx; @@ -851,14 +851,10 @@ (!currentFidx, fdec.svar.vname) (Util.list_map (fun (fn, _, _) -> fn) (argsToList args)); fdec.svar.vreferenced <- false; - (* Force inline functions to be static. *) - (* GN: This turns out to be wrong. inline functions are external, - unless specified to be static. *) - (* - if fdec.svar.vinline && fdec.svar.vstorage = NoStorage then - fdec.svar.vstorage <- Static; - *) - if fdec.svar.vstorage <> Static then + (* C99: inline functions are internal unless specified to be external *) + (* GNU89: inline functions are external unless specified to be static *) + if fdec.svar.vstorage <> Static && (not fdec.svar.vinline || fdec.svar.vstorage = Extern) then + (* function with external linkage *) matchVarinfo fdec.svar (l, !currentDeclIdx) else if fdec.svar.vinline && !merge_inlines then (* Just create the nodes for inline functions *) @@ -1334,7 +1330,9 @@ (* Process a varinfo. Reuse an old one, or rename it if necessary *) let processVarinfo (vi : varinfo) (vloc : location) : varinfo = if vi.vreferenced then vi (* Already done *) - else if vi.vstorage = Static || (vi.vinline && not (!merge_inlines)) then + else if vi.vstorage = Static || vi.vinline then + (* rename inlines no matter if merge_inlines is enabled or not, + renaming is undone using originalVarNames in case merging is successful *) ( (* Maybe it is static or inline and we are not merging inlines. Rename it then *) let newName, _ = A.newAlphaName ~alphaTable:vtAlpha ~undolist:None ~lookupname:vi.vname ~data:!currentLoc in diff --git a/test/testcil.pl b/test/testcil.pl index 40dcfe196..b3cff69e7 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -701,6 +701,18 @@ sub addToGroup { addTest("testrunc99/c99-fixed-width-int"); addTest("combinec99inline"); addBadComment("combinec99inline", "C99 inline semantic not fully supported."); +addTest("combinec99inline1"); +addTest("combinec99inline2"); +addTest("combinec99inline3"); +addTest("combinec99inline4"); +addTest("combinec99inline5"); +addTest("combinec99inline6"); +addTest("combinec99mergeinline1"); +addTest("combinec99mergeinline2"); +addTest("combinec99mergeinline3"); +addTest("combinec99mergeinline4"); +addTest("combinec99mergeinline5"); +addTest("combinec99mergeinline6"); addTest("testrunc11/c11-generic"); addTest("testrunc11/c11-caserange"); From 5af589d11867a3c2ba28594bfd8dee316e95a91e Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Tue, 8 Nov 2022 14:16:11 +0100 Subject: [PATCH 03/15] inline semantics based on c99mode --- src/ciloptions.ml | 2 +- src/cilutil.ml | 2 +- src/mergecil.ml | 15 ++++++++++----- 3 files changed, 12 insertions(+), 7 deletions(-) diff --git a/src/ciloptions.ml b/src/ciloptions.ml index 178822940..f03f7c3f8 100644 --- a/src/ciloptions.ml +++ b/src/ciloptions.ml @@ -167,7 +167,7 @@ let options : (string * Arg.spec * string) list = " Same as --check, but treats problems as errors not warnings."; "", Arg.Unit (fun _ -> ()), ""; - "--mergeinlines", Arg.Unit (fun _ -> Cilutil.merge_inlines := true), + "--mergeinlines", Arg.Unit (fun _ -> Mergecil.merge_inlines := true), " Try to merge definitions of inline functions. They can appear in multiple files and we would like them all to be the same. This can slow down the merger an order of magnitude."; diff --git a/src/cilutil.ml b/src/cilutil.ml index b8bd102b1..3ee492ebf 100644 --- a/src/cilutil.ml +++ b/src/cilutil.ml @@ -50,4 +50,4 @@ let sliceGlobal = ref false let printStages = ref false -let merge_inlines = ref false +let c99Mode = ref false diff --git a/src/mergecil.ml b/src/mergecil.ml index 67465b634..c224f30f6 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -62,7 +62,7 @@ (* Try to merge definitions of inline functions. They can appear in multiple files and we would like them all to be the same. This can slow down the merger an order of magnitude !!! *) - let merge_inlines = Cilutil.merge_inlines + let merge_inlines = ref false let mergeInlinesRepeat () = !merge_inlines && true let mergeInlinesWithAlphaConvert () = !merge_inlines && true @@ -71,6 +71,13 @@ but only probabilistically accurate *) let mergeGlobals = true + (* C99: inline functions are internal unless specified to be external + GNU89: inline functions are external unless specified to be static or extern + GNU89 inline semantics is used also when gnu_inline attribute is present on all inline declarations *) + let externallyVisible vi = vi.vstorage <> Static + && ((!Cilutil.c99Mode && (not vi.vinline || vi.vstorage = Extern)) + || ((not !Cilutil.c99Mode || hasAttribute "gnu_inline" (typeAttrs vi.vtype)) && (not vi.vinline || vi.vstorage <> Extern))) + (* Return true if 's' starts with the prefix 'p' *) let prefix p s = let lp = String.length p in @@ -841,7 +848,7 @@ currentLoc := l; incr currentDeclIdx; vi.vreferenced <- false; - if vi.vstorage <> Static && (not vi.vinline || vi.vstorage = Extern) then matchVarinfo vi (l, !currentDeclIdx) + if externallyVisible vi then matchVarinfo vi (l, !currentDeclIdx) | GFun (fdec, l) -> currentLoc := l; incr currentDeclIdx; @@ -851,9 +858,7 @@ (!currentFidx, fdec.svar.vname) (Util.list_map (fun (fn, _, _) -> fn) (argsToList args)); fdec.svar.vreferenced <- false; - (* C99: inline functions are internal unless specified to be external *) - (* GNU89: inline functions are external unless specified to be static *) - if fdec.svar.vstorage <> Static && (not fdec.svar.vinline || fdec.svar.vstorage = Extern) then + if externallyVisible fdec.svar then (* function with external linkage *) matchVarinfo fdec.svar (l, !currentDeclIdx) else if fdec.svar.vinline && !merge_inlines then From 96f7a07d84ede4d691ef39e45ac01aa5ee871054 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Wed, 9 Nov 2022 16:39:56 +0100 Subject: [PATCH 04/15] remove leftovers of msvcMode --- src/cil.ml | 7 ------- src/cil.mli | 4 ---- 2 files changed, 11 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index e42bc08eb..c68316499 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -55,10 +55,6 @@ module IH = Inthash information in configure.in *) let cilVersion = Cilversion.cilVersion -(* A few globals that control the interpretation of C source *) -let msvcMode = ref false (* Whether the pretty printer should - print output for the MS VC - compiler. Default is GCC *) let c99Mode = ref true (* True to handle ISO C 99 vs 90 changes. c99mode only affects parsing of decimal integer constants without suffix a) on machines where long and long long do not have the same size @@ -4302,9 +4298,6 @@ class defaultCilPrinterClass : cilPrinter = object (self) | "complex", [] -> text "__complex__", false | "aconst", [] -> text "__const__", true | "thread", [] -> text "__thread", false -(* - | "used", [] when not !msvcMode -> text "__attribute_used__", false -*) | "volatile", [] -> text "volatile", false | "restrict", [] -> text "__restrict", false | "missingproto", [] -> text "/* missing proto */", false diff --git a/src/cil.mli b/src/cil.mli index 1079bc606..7fb0de833 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -2021,10 +2021,6 @@ val visitCilAttributes: cilVisitor -> attribute list -> attribute list (** {b Utility functions} *) -(** Whether the pretty printer should print output for the MS VC compiler. - Default is GCC. After you set this function you should call {!initCIL}. *) -val msvcMode: bool ref - (** Whether to convert local static variables into global static variables *) val makeStaticGlobal: bool ref From 53d5ab0ae621fbd6387daa39235bb67672d94841 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 14 Nov 2022 11:37:42 +0100 Subject: [PATCH 05/15] set cstd based on gcc parameters --- doc/cil.tex | 6 +++++- lib/perl5/App/Cilly.pm.in | 41 ++++++++++++++++++++++++++++++++++----- lib/perl5/patcher | 7 +++---- src/ciloptions.ml | 3 +++ src/cilutil.ml | 9 ++++++++- src/mergecil.ml | 5 +++-- test/Makefile | 2 +- 7 files changed, 59 insertions(+), 14 deletions(-) diff --git a/doc/cil.tex b/doc/cil.tex index 85b6a6da0..48ebb8356 100644 --- a/doc/cil.tex +++ b/doc/cil.tex @@ -2357,7 +2357,11 @@ \subsection{Effects of the CIL translation} --mode=xxx What tool to emulate: GNUCC - GNU CC MSVC - MS VC cl compiler - + --cstd=xxx What C standard / GNU dialect to emulate: + c90 (also used for c89, iso9899:1990, iso9899:199409, gnu90, gnu89) + c99 (also used for c9x, iso9899:1999, iso9899:199x, gnu99, gnu9x) + c11 (c1x, iso9899:2011, c17, c18, iso9899:2017, iso9899:2018, c2x, gnu11, gnu1x, gnu17, gnu18, gnu2x) + gnu89inline (gnu89 only for inline) --dest=xxx The destination directory. Will make one if it does not exist --patch=xxx Patch file (can be specified multiple times) --ppargs=xxx An argument to be passed to the preprocessor (can be specified diff --git a/lib/perl5/App/Cilly.pm.in b/lib/perl5/App/Cilly.pm.in index 2baff1570..582b67ab0 100644 --- a/lib/perl5/App/Cilly.pm.in +++ b/lib/perl5/App/Cilly.pm.in @@ -215,6 +215,10 @@ sub collectOneArgument { if($arg eq "--verbose") { $self->{VERBOSE} = 1; return 1; } + if($arg eq "--cstd=(.+)\$") { + push @{$self->{CILARGS}}, $1; + return 1; + } if($arg eq "--flatten_linker_scripts") { $self->{FLATTEN_LINKER_SCRIPTS} = 1; return 1; } @@ -361,6 +365,11 @@ Options: AR - GNU ar This option must be the first one! If it is not found there then GNUCC mode is assumed. + --cstd=xxx What C standard / GNU dialect to emulate: + c90 (also used for c89, iso9899:1990, iso9899:199409, gnu90, gnu89) + c99 (also used for c9x, iso9899:1999, iso9899:199x, gnu99, gnu9x) + c11 (c1x, iso9899:2011, c17, c18, iso9899:2017, iso9899:2018, c2x, gnu11, gnu1x, gnu17, gnu18, gnu2x) + gnu89inline (gnu89 only for inline) --help (or -help) Prints this help message. --verbose Prints a lot of information about what is being done. --save-temps Keep temporary files in the current directory. @@ -1517,12 +1526,34 @@ sub new { # skipping -###, --help, --target-help, --version # C Language Options - "-ansi" => { TYPE => 'ALLARGS' }, - '-std=' => { TYPE => 'ALLARGS' }, + "-ansi" => { + TYPE => 'ALLARGS', + RUN => sub { + push @{$stub->{CILARGS}}, "--std", "c90"; + }}, + "-std=(c90|c89|iso9899:1990|iso9899:199409|gnu90|gnu89))" => { + TYPE => 'ALLARGS', + RUN => sub { + push @{$stub->{CILARGS}}, "--std", "c90"; + }}, + "-std=(c99|c9x|iso9899:1999|iso9899:199x|gnu99|gnu9x)" => { + TYPE => 'ALLARGS', + RUN => sub { + push @{$stub->{CILARGS}}, "--std", "c99"; + }}, + "-std=(c1x|iso9899:2011|c17|c18|iso9899:2017|iso9899:2018|c2x|gnu11|gnu1x|gnu17|gnu18|gnu2x)" => { + TYPE => 'ALLARGS', + RUN => sub { + push @{$stub->{CILARGS}}, "--std", "c11"; + }}, + "-fgnu89-inline" => { + RUN => sub { + push @{$stub->{CILARGS}}, "--std", "gnu89inline"; + }}, "-aux-info\$" => { TYPE => 'CC', ONEMORE => 1 }, - # GCC might define some more macros, eg. for -fPIC, so pass - # the -f to the preprocessor and the compiler - "-f" => { TYPE => 'ALLARGS' }, + # GCC might define some more macros, eg. for -fPIC, so pass + # the -f to the preprocessor and the compiler + "-f" => { TYPE => 'ALLARGS' }, # -Wx,blah options (placed before general -W warning options) #matth: the handling of -Wp may be wrong. We may need to diff --git a/lib/perl5/patcher b/lib/perl5/patcher index 081b776f2..665d133b4 100755 --- a/lib/perl5/patcher +++ b/lib/perl5/patcher @@ -66,7 +66,6 @@ options: --verbose Prints a lot of information about what is being done --mode=xxx What tool to emulate: GNUCC - GNU CC - --dest=xxx The destination directory. Will make one if it does not exist --patch=xxx Patch file (can be specified multiple times) @@ -94,9 +93,9 @@ my %option; "--verbose|v", # Display information about programs invoked "--mode=s", # The mode (GNUCC) "--dest=s", # The destination directory - "--patch=s@", # Patch files - "--ufile=s@", # User include files - "--sfile=s@", # System include files + "--patch=s@", # Patch files + "--ufile=s@", # User include files + "--sfile=s@", # System include files "--stdoutpp", # pp to stdout "--skipmissing", "--dumpversion", diff --git a/src/ciloptions.ml b/src/ciloptions.ml index f03f7c3f8..601cd8ee6 100644 --- a/src/ciloptions.ml +++ b/src/ciloptions.ml @@ -167,6 +167,9 @@ let options : (string * Arg.spec * string) list = " Same as --check, but treats problems as errors not warnings."; "", Arg.Unit (fun _ -> ()), ""; + "--cstd", Arg.String (fun s -> Cilutil.cstd := Cilutil.cstd_of_string s), + " Specify the c language standard. Choose between c90, c99, c11 and gnu89inline"; + "--mergeinlines", Arg.Unit (fun _ -> Mergecil.merge_inlines := true), " Try to merge definitions of inline functions. They can appear in multiple files and we would like them all to be the same. This can slow down the diff --git a/src/cilutil.ml b/src/cilutil.ml index 3ee492ebf..ec65b9e12 100644 --- a/src/cilutil.ml +++ b/src/cilutil.ml @@ -50,4 +50,11 @@ let sliceGlobal = ref false let printStages = ref false -let c99Mode = ref false +type cstd = C90 | C99 | C11 | Gnu89inline +let cstd_of_string = function +| "c90" -> C90 +| "c99" -> C99 +| "c11" -> C11 +| "gnu89inline" -> Gnu89inline +| _ -> failwith "Not a valid c standard argument." +let cstd = ref C99 diff --git a/src/mergecil.ml b/src/mergecil.ml index c224f30f6..3170c7ca5 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -75,8 +75,9 @@ GNU89: inline functions are external unless specified to be static or extern GNU89 inline semantics is used also when gnu_inline attribute is present on all inline declarations *) let externallyVisible vi = vi.vstorage <> Static - && ((!Cilutil.c99Mode && (not vi.vinline || vi.vstorage = Extern)) - || ((not !Cilutil.c99Mode || hasAttribute "gnu_inline" (typeAttrs vi.vtype)) && (not vi.vinline || vi.vstorage <> Extern))) + && ((!Cilutil.cstd <> C90 && !Cilutil.cstd <> Gnu89inline && (not vi.vinline || vi.vstorage = Extern)) + || ((!Cilutil.cstd == C90 || !Cilutil.cstd == Gnu89inline || hasAttribute "gnu_inline" (typeAttrs vi.vtype)) + && (not vi.vinline || vi.vstorage <> Extern))) (* Return true if 's' starts with the prefix 'p' *) let prefix p s = diff --git a/test/Makefile b/test/Makefile index 914c860f9..67f0be6be 100644 --- a/test/Makefile +++ b/test/Makefile @@ -289,7 +289,7 @@ combine%: $(SMALL1)/combine%_1.c combinegnuinline: cd $(SMALL1); \ - $(CILLY) --merge $(CFLAGS) -std=gnu90 -fcommon \ + $(CILLY) --merge $(CFLAGS) -std=gnu90 -fcommon \ combinegnuinline_1.c combinegnuinline_2.c \ $(EXEOUT)combinegnuinline.exe cd $(SMALL1); ./combinegnuinline.exe From f0799af0f09d650ad3c65ecb1c17885b035d43ab Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 14 Nov 2022 11:56:29 +0100 Subject: [PATCH 06/15] fixes --- lib/perl5/App/Cilly.pm.in | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/lib/perl5/App/Cilly.pm.in b/lib/perl5/App/Cilly.pm.in index 582b67ab0..5ae10f925 100644 --- a/lib/perl5/App/Cilly.pm.in +++ b/lib/perl5/App/Cilly.pm.in @@ -1529,26 +1529,26 @@ sub new { "-ansi" => { TYPE => 'ALLARGS', RUN => sub { - push @{$stub->{CILARGS}}, "--std", "c90"; + push @{$stub->{CILARGS}}, "--cstd", "c90"; }}, - "-std=(c90|c89|iso9899:1990|iso9899:199409|gnu90|gnu89))" => { + "-std=(c90|c89|iso9899:1990|iso9899:199409|gnu90|gnu89)" => { TYPE => 'ALLARGS', RUN => sub { - push @{$stub->{CILARGS}}, "--std", "c90"; + push @{$stub->{CILARGS}}, "--cstd", "c90"; }}, "-std=(c99|c9x|iso9899:1999|iso9899:199x|gnu99|gnu9x)" => { TYPE => 'ALLARGS', RUN => sub { - push @{$stub->{CILARGS}}, "--std", "c99"; + push @{$stub->{CILARGS}}, "--cstd", "c99"; }}, "-std=(c1x|iso9899:2011|c17|c18|iso9899:2017|iso9899:2018|c2x|gnu11|gnu1x|gnu17|gnu18|gnu2x)" => { TYPE => 'ALLARGS', RUN => sub { - push @{$stub->{CILARGS}}, "--std", "c11"; + push @{$stub->{CILARGS}}, "--cstd", "c11"; }}, "-fgnu89-inline" => { RUN => sub { - push @{$stub->{CILARGS}}, "--std", "gnu89inline"; + push @{$stub->{CILARGS}}, "--cstd", "gnu89inline"; }}, "-aux-info\$" => { TYPE => 'CC', ONEMORE => 1 }, # GCC might define some more macros, eg. for -fPIC, so pass From 0777acbf7121eeda444efc1385cab7e96f7fac9b Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 14 Nov 2022 13:31:14 +0100 Subject: [PATCH 07/15] add tests for inline gnu89 vs c99 --- test/small1/combine-c99inline7_1.c | 3 +++ test/small1/combine-c99inline7_2.c | 3 +++ test/small1/combine-c99inline7_3.c | 5 +++++ test/small1/combine23_1.c | 3 +++ test/small1/combine23_2.c | 3 +++ test/small1/combine23_3.c | 5 +++++ test/testcil.pl | 2 ++ 7 files changed, 24 insertions(+) create mode 100644 test/small1/combine-c99inline7_1.c create mode 100644 test/small1/combine-c99inline7_2.c create mode 100644 test/small1/combine-c99inline7_3.c create mode 100644 test/small1/combine23_1.c create mode 100644 test/small1/combine23_2.c create mode 100644 test/small1/combine23_3.c diff --git a/test/small1/combine-c99inline7_1.c b/test/small1/combine-c99inline7_1.c new file mode 100644 index 000000000..218ab7327 --- /dev/null +++ b/test/small1/combine-c99inline7_1.c @@ -0,0 +1,3 @@ +inline int add(int i, int j) { + return i - j; +} diff --git a/test/small1/combine-c99inline7_2.c b/test/small1/combine-c99inline7_2.c new file mode 100644 index 000000000..bf3d29197 --- /dev/null +++ b/test/small1/combine-c99inline7_2.c @@ -0,0 +1,3 @@ +extern inline int add(int i, int j) { + return i + j; +} diff --git a/test/small1/combine-c99inline7_3.c b/test/small1/combine-c99inline7_3.c new file mode 100644 index 000000000..599c3576a --- /dev/null +++ b/test/small1/combine-c99inline7_3.c @@ -0,0 +1,5 @@ +int add(); + +int main() { + return add(-3, 3); +} diff --git a/test/small1/combine23_1.c b/test/small1/combine23_1.c new file mode 100644 index 000000000..5b5f19aaa --- /dev/null +++ b/test/small1/combine23_1.c @@ -0,0 +1,3 @@ +inline int add(int i, int j) { + return i + j; +} diff --git a/test/small1/combine23_2.c b/test/small1/combine23_2.c new file mode 100644 index 000000000..07f5101ac --- /dev/null +++ b/test/small1/combine23_2.c @@ -0,0 +1,3 @@ +extern inline int add(int i, int j) { + return i - j; +} diff --git a/test/small1/combine23_3.c b/test/small1/combine23_3.c new file mode 100644 index 000000000..599c3576a --- /dev/null +++ b/test/small1/combine23_3.c @@ -0,0 +1,5 @@ +int add(); + +int main() { + return add(-3, 3); +} diff --git a/test/testcil.pl b/test/testcil.pl index b3cff69e7..f3b9d74a9 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -432,6 +432,7 @@ sub addToGroup { addTest("combine21 "); addTest("combine22 "); addBadComment("combine22", "Bug. Outstanding since 1.3.6 at least"); +addTest("combine23 "); addTest("combinealias "); addTest("combinelibrik "); addTest("combineenum1 "); @@ -707,6 +708,7 @@ sub addToGroup { addTest("combinec99inline4"); addTest("combinec99inline5"); addTest("combinec99inline6"); +addTest("combinec99inline7"); addTest("combinec99mergeinline1"); addTest("combinec99mergeinline2"); addTest("combinec99mergeinline3"); From 2f8df898399175c30d480d9e986327f8626a5ba4 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 14 Nov 2022 14:20:19 +0100 Subject: [PATCH 08/15] add some more tests --- test/small1/combine-c99-mergeinline7.h | 3 +++ test/small1/combine-c99-mergeinline7_1.c | 1 + test/small1/combine-c99-mergeinline7_2.c | 5 +++++ test/small1/combine-c99inline8_1.c | 5 +++++ test/small1/combine-c99inline8_2.c | 3 +++ test/small1/combine-c99inline8_3.c | 3 +++ test/small1/combine-c99inline9.h | 3 +++ test/small1/combine-c99inline9_1.c | 1 + test/small1/combine-c99inline9_2.c | 5 +++++ test/small1/combine-c99inline_2.c | 4 +++- test/testcil.pl | 3 +++ 11 files changed, 35 insertions(+), 1 deletion(-) create mode 100644 test/small1/combine-c99-mergeinline7.h create mode 100644 test/small1/combine-c99-mergeinline7_1.c create mode 100644 test/small1/combine-c99-mergeinline7_2.c create mode 100644 test/small1/combine-c99inline8_1.c create mode 100644 test/small1/combine-c99inline8_2.c create mode 100644 test/small1/combine-c99inline8_3.c create mode 100644 test/small1/combine-c99inline9.h create mode 100644 test/small1/combine-c99inline9_1.c create mode 100644 test/small1/combine-c99inline9_2.c diff --git a/test/small1/combine-c99-mergeinline7.h b/test/small1/combine-c99-mergeinline7.h new file mode 100644 index 000000000..5b5f19aaa --- /dev/null +++ b/test/small1/combine-c99-mergeinline7.h @@ -0,0 +1,3 @@ +inline int add(int i, int j) { + return i + j; +} diff --git a/test/small1/combine-c99-mergeinline7_1.c b/test/small1/combine-c99-mergeinline7_1.c new file mode 100644 index 000000000..618f7ad80 --- /dev/null +++ b/test/small1/combine-c99-mergeinline7_1.c @@ -0,0 +1 @@ +#include "combine-c99-mergeinline7.h" diff --git a/test/small1/combine-c99-mergeinline7_2.c b/test/small1/combine-c99-mergeinline7_2.c new file mode 100644 index 000000000..c4fa3cb4e --- /dev/null +++ b/test/small1/combine-c99-mergeinline7_2.c @@ -0,0 +1,5 @@ +#include "combine-c99-mergeinline7.h" + +int main() { + return add(-3, 3); +} diff --git a/test/small1/combine-c99inline8_1.c b/test/small1/combine-c99inline8_1.c new file mode 100644 index 000000000..599c3576a --- /dev/null +++ b/test/small1/combine-c99inline8_1.c @@ -0,0 +1,5 @@ +int add(); + +int main() { + return add(-3, 3); +} diff --git a/test/small1/combine-c99inline8_2.c b/test/small1/combine-c99inline8_2.c new file mode 100644 index 000000000..bf3d29197 --- /dev/null +++ b/test/small1/combine-c99inline8_2.c @@ -0,0 +1,3 @@ +extern inline int add(int i, int j) { + return i + j; +} diff --git a/test/small1/combine-c99inline8_3.c b/test/small1/combine-c99inline8_3.c new file mode 100644 index 000000000..218ab7327 --- /dev/null +++ b/test/small1/combine-c99inline8_3.c @@ -0,0 +1,3 @@ +inline int add(int i, int j) { + return i - j; +} diff --git a/test/small1/combine-c99inline9.h b/test/small1/combine-c99inline9.h new file mode 100644 index 000000000..5b5f19aaa --- /dev/null +++ b/test/small1/combine-c99inline9.h @@ -0,0 +1,3 @@ +inline int add(int i, int j) { + return i + j; +} diff --git a/test/small1/combine-c99inline9_1.c b/test/small1/combine-c99inline9_1.c new file mode 100644 index 000000000..663c387f1 --- /dev/null +++ b/test/small1/combine-c99inline9_1.c @@ -0,0 +1 @@ +#include "combine-c99inline9.h" diff --git a/test/small1/combine-c99inline9_2.c b/test/small1/combine-c99inline9_2.c new file mode 100644 index 000000000..501df64b0 --- /dev/null +++ b/test/small1/combine-c99inline9_2.c @@ -0,0 +1,5 @@ +#include "combine-c99inline9.h" + +int main() { + return add(-3, 3); +} diff --git a/test/small1/combine-c99inline_2.c b/test/small1/combine-c99inline_2.c index 521031bd3..0e8b4c4ee 100644 --- a/test/small1/combine-c99inline_2.c +++ b/test/small1/combine-c99inline_2.c @@ -1,5 +1,7 @@ #include "stdio.h" -inline void add(int i, int j) { printf("Called inline\n"); } +inline void add(int i, int j) { + printf("Called inline\n"); +} int main() { add(4, 5); diff --git a/test/testcil.pl b/test/testcil.pl index f3b9d74a9..55982ff42 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -709,12 +709,15 @@ sub addToGroup { addTest("combinec99inline5"); addTest("combinec99inline6"); addTest("combinec99inline7"); +addTest("combinec99inline8"); +addTest("combinec99inline9"); addTest("combinec99mergeinline1"); addTest("combinec99mergeinline2"); addTest("combinec99mergeinline3"); addTest("combinec99mergeinline4"); addTest("combinec99mergeinline5"); addTest("combinec99mergeinline6"); +addTest("combinec99mergeinline7"); addTest("testrunc11/c11-generic"); addTest("testrunc11/c11-caserange"); From 77754f07cdef6469969a3ac411fea3e0950fac45 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Mon, 14 Nov 2022 14:21:50 +0100 Subject: [PATCH 09/15] fix: rename only non-external inline functions --- src/mergecil.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/mergecil.ml b/src/mergecil.ml index 3170c7ca5..ad0321f08 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -1336,8 +1336,8 @@ (* Process a varinfo. Reuse an old one, or rename it if necessary *) let processVarinfo (vi : varinfo) (vloc : location) : varinfo = if vi.vreferenced then vi (* Already done *) - else if vi.vstorage = Static || vi.vinline then - (* rename inlines no matter if merge_inlines is enabled or not, + else if not (externallyVisible vi) then + (* rename static and not-external inline functions no matter if merge_inlines is enabled or not, renaming is undone using originalVarNames in case merging is successful *) ( (* Maybe it is static or inline and we are not merging inlines. Rename it then *) From 6bd94147bdc4df0434085d210a839b8ca092606a Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Tue, 15 Nov 2022 14:48:28 +0100 Subject: [PATCH 10/15] set float c99mode based on cstd --- src/cil.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cil.ml b/src/cil.ml index c68316499..859662d76 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -55,7 +55,7 @@ module IH = Inthash information in configure.in *) let cilVersion = Cilversion.cilVersion -let c99Mode = ref true (* True to handle ISO C 99 vs 90 changes. +let c99Mode = ref (!Cilutil.cstd <> Cilutil.C90) (* True to handle ISO C 99 vs 90 changes. c99mode only affects parsing of decimal integer constants without suffix a) on machines where long and long long do not have the same size (e.g. 32 Bit machines, 64 Bit Windows, not 64 Bit MacOS or (most? all?) 64 Bit Linux): From 6c0272f016050eb64c07ed9e2b7ae45239e895e0 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Fri, 18 Nov 2022 14:19:42 +0100 Subject: [PATCH 11/15] separate flag for gnu89inline --- doc/cil.tex | 2 +- lib/perl5/App/Cilly.pm.in | 4 ++-- src/cil.ml | 6 +++--- src/ciloptions.ml | 5 ++++- src/cilutil.ml | 4 ++-- src/mergecil.ml | 4 ++-- 6 files changed, 14 insertions(+), 11 deletions(-) diff --git a/doc/cil.tex b/doc/cil.tex index 48ebb8356..156010005 100644 --- a/doc/cil.tex +++ b/doc/cil.tex @@ -2361,7 +2361,7 @@ \subsection{Effects of the CIL translation} c90 (also used for c89, iso9899:1990, iso9899:199409, gnu90, gnu89) c99 (also used for c9x, iso9899:1999, iso9899:199x, gnu99, gnu9x) c11 (c1x, iso9899:2011, c17, c18, iso9899:2017, iso9899:2018, c2x, gnu11, gnu1x, gnu17, gnu18, gnu2x) - gnu89inline (gnu89 only for inline) + --gnu89inline gnu89 semantic for inline functions --dest=xxx The destination directory. Will make one if it does not exist --patch=xxx Patch file (can be specified multiple times) --ppargs=xxx An argument to be passed to the preprocessor (can be specified diff --git a/lib/perl5/App/Cilly.pm.in b/lib/perl5/App/Cilly.pm.in index 5ae10f925..01cf7737e 100644 --- a/lib/perl5/App/Cilly.pm.in +++ b/lib/perl5/App/Cilly.pm.in @@ -369,7 +369,7 @@ Options: c90 (also used for c89, iso9899:1990, iso9899:199409, gnu90, gnu89) c99 (also used for c9x, iso9899:1999, iso9899:199x, gnu99, gnu9x) c11 (c1x, iso9899:2011, c17, c18, iso9899:2017, iso9899:2018, c2x, gnu11, gnu1x, gnu17, gnu18, gnu2x) - gnu89inline (gnu89 only for inline) + --gnu89inline gnu89 semantic for inline functions --help (or -help) Prints this help message. --verbose Prints a lot of information about what is being done. --save-temps Keep temporary files in the current directory. @@ -1548,7 +1548,7 @@ sub new { }}, "-fgnu89-inline" => { RUN => sub { - push @{$stub->{CILARGS}}, "--cstd", "gnu89inline"; + push @{$stub->{CILARGS}}, "--gnu89inline"; }}, "-aux-info\$" => { TYPE => 'CC', ONEMORE => 1 }, # GCC might define some more macros, eg. for -fPIC, so pass diff --git a/src/cil.ml b/src/cil.ml index 859662d76..60603ba8d 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -55,7 +55,7 @@ module IH = Inthash information in configure.in *) let cilVersion = Cilversion.cilVersion -let c99Mode = ref (!Cilutil.cstd <> Cilutil.C90) (* True to handle ISO C 99 vs 90 changes. +let c99Mode () = !Cilutil.cstd <> Cilutil.C90 (* True to handle ISO C 99 vs 90 changes. c99mode only affects parsing of decimal integer constants without suffix a) on machines where long and long long do not have the same size (e.g. 32 Bit machines, 64 Bit Windows, not 64 Bit MacOS or (most? all?) 64 Bit Linux): @@ -2771,7 +2771,7 @@ let parseInt (str: string) : exp = 1, [IUInt; IULong; IULongLong] else 0, if octalhex then [IInt; IUInt; ILong; IULong; ILongLong; IULongLong] - else if not !c99Mode then [ IInt; ILong; IULong; ILongLong; IULongLong] + else if not (c99Mode ()) then [ IInt; ILong; IULong; ILongLong; IULongLong] else [IInt; ILong; ILongLong] (* c99mode only affects parsing of decimal integer constants without suffix a) on machines where long and long long do not have the same size @@ -4294,7 +4294,7 @@ class defaultCilPrinterClass : cilPrinter = object (self) | "const", [] -> nil, false (* don't print const directly, because of split local declarations *) | "pconst", [] -> text "const", false (* pconst means print const *) (* Put the aconst inside the attribute list *) - | "complex", [] when !c99Mode -> text "_Complex", false + | "complex", [] when (c99Mode ()) -> text "_Complex", false | "complex", [] -> text "__complex__", false | "aconst", [] -> text "__const__", true | "thread", [] -> text "__thread", false diff --git a/src/ciloptions.ml b/src/ciloptions.ml index 601cd8ee6..56328decb 100644 --- a/src/ciloptions.ml +++ b/src/ciloptions.ml @@ -168,7 +168,10 @@ let options : (string * Arg.spec * string) list = "", Arg.Unit (fun _ -> ()), ""; "--cstd", Arg.String (fun s -> Cilutil.cstd := Cilutil.cstd_of_string s), - " Specify the c language standard. Choose between c90, c99, c11 and gnu89inline"; + " Specify the c language standard. Choose between c90, c99, c11"; + + "--gnu89inline", Arg.Set Cilutil.gnu89inline, + "Use gnu89 semantic for inlining"; "--mergeinlines", Arg.Unit (fun _ -> Mergecil.merge_inlines := true), " Try to merge definitions of inline functions. They can appear in multiple diff --git a/src/cilutil.ml b/src/cilutil.ml index ec65b9e12..6f7ab7bb5 100644 --- a/src/cilutil.ml +++ b/src/cilutil.ml @@ -50,11 +50,11 @@ let sliceGlobal = ref false let printStages = ref false -type cstd = C90 | C99 | C11 | Gnu89inline +type cstd = C90 | C99 | C11 let cstd_of_string = function | "c90" -> C90 | "c99" -> C99 | "c11" -> C11 -| "gnu89inline" -> Gnu89inline | _ -> failwith "Not a valid c standard argument." let cstd = ref C99 +let gnu89inline = ref false diff --git a/src/mergecil.ml b/src/mergecil.ml index ad0321f08..95e40e571 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -75,8 +75,8 @@ GNU89: inline functions are external unless specified to be static or extern GNU89 inline semantics is used also when gnu_inline attribute is present on all inline declarations *) let externallyVisible vi = vi.vstorage <> Static - && ((!Cilutil.cstd <> C90 && !Cilutil.cstd <> Gnu89inline && (not vi.vinline || vi.vstorage = Extern)) - || ((!Cilutil.cstd == C90 || !Cilutil.cstd == Gnu89inline || hasAttribute "gnu_inline" (typeAttrs vi.vtype)) + && ((!Cilutil.cstd <> C90 && not !Cilutil.gnu89inline && (not vi.vinline || vi.vstorage = Extern)) + || ((!Cilutil.cstd == C90 || !Cilutil.gnu89inline || hasAttribute "gnu_inline" (typeAttrs vi.vtype)) && (not vi.vinline || vi.vstorage <> Extern))) (* Return true if 's' starts with the prefix 'p' *) From 7208e8b90dc7c0f29f76a0afb4e2ccb2f6685c26 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Fri, 18 Nov 2022 14:52:49 +0100 Subject: [PATCH 12/15] move options to cil --- src/cil.ml | 10 +++++++++- src/cil.mli | 5 +++++ src/ciloptions.ml | 4 ++-- src/cilutil.ml | 9 --------- src/mergecil.ml | 4 ++-- 5 files changed, 18 insertions(+), 14 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 60603ba8d..8a800e67f 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -55,7 +55,15 @@ module IH = Inthash information in configure.in *) let cilVersion = Cilversion.cilVersion -let c99Mode () = !Cilutil.cstd <> Cilutil.C90 (* True to handle ISO C 99 vs 90 changes. +type cstd = C90 | C99 | C11 +let cstd_of_string = function +| "c90" -> C90 +| "c99" -> C99 +| "c11" -> C11 +| _ -> failwith "Not a valid c standard argument." +let cstd = ref C99 +let gnu89inline = ref false +let c99Mode () = !cstd <> C90 (* True to handle ISO C 99 vs 90 changes. c99mode only affects parsing of decimal integer constants without suffix a) on machines where long and long long do not have the same size (e.g. 32 Bit machines, 64 Bit Windows, not 64 Bit MacOS or (most? all?) 64 Bit Linux): diff --git a/src/cil.mli b/src/cil.mli index 7fb0de833..19dbac063 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -53,6 +53,11 @@ val initCIL: unit -> unit M.m.r (major, minor and release) *) val cilVersion: string +type cstd = C90 | C99 | C11 +val cstd_of_string: string -> cstd +val cstd: cstd ref +val gnu89inline: bool ref + (** This module defines the abstract syntax of CIL. It also provides utility functions for traversing the CIL data structures, and pretty-printing them. The parser can be invoked as diff --git a/src/ciloptions.ml b/src/ciloptions.ml index 56328decb..ada3e1ef1 100644 --- a/src/ciloptions.ml +++ b/src/ciloptions.ml @@ -167,10 +167,10 @@ let options : (string * Arg.spec * string) list = " Same as --check, but treats problems as errors not warnings."; "", Arg.Unit (fun _ -> ()), ""; - "--cstd", Arg.String (fun s -> Cilutil.cstd := Cilutil.cstd_of_string s), + "--cstd", Arg.String (fun s -> Cil.cstd := Cil.cstd_of_string s), " Specify the c language standard. Choose between c90, c99, c11"; - "--gnu89inline", Arg.Set Cilutil.gnu89inline, + "--gnu89inline", Arg.Set Cil.gnu89inline, "Use gnu89 semantic for inlining"; "--mergeinlines", Arg.Unit (fun _ -> Mergecil.merge_inlines := true), diff --git a/src/cilutil.ml b/src/cilutil.ml index 6f7ab7bb5..1aa0b02bc 100644 --- a/src/cilutil.ml +++ b/src/cilutil.ml @@ -49,12 +49,3 @@ let sliceGlobal = ref false let printStages = ref false - -type cstd = C90 | C99 | C11 -let cstd_of_string = function -| "c90" -> C90 -| "c99" -> C99 -| "c11" -> C11 -| _ -> failwith "Not a valid c standard argument." -let cstd = ref C99 -let gnu89inline = ref false diff --git a/src/mergecil.ml b/src/mergecil.ml index 95e40e571..c00d9d614 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -75,8 +75,8 @@ GNU89: inline functions are external unless specified to be static or extern GNU89 inline semantics is used also when gnu_inline attribute is present on all inline declarations *) let externallyVisible vi = vi.vstorage <> Static - && ((!Cilutil.cstd <> C90 && not !Cilutil.gnu89inline && (not vi.vinline || vi.vstorage = Extern)) - || ((!Cilutil.cstd == C90 || !Cilutil.gnu89inline || hasAttribute "gnu_inline" (typeAttrs vi.vtype)) + && ((!Cil.cstd <> Cil.C90 && not !Cil.gnu89inline && (not vi.vinline || vi.vstorage = Extern)) + || ((!Cil.cstd == Cil.C90 || !Cil.gnu89inline || hasAttribute "gnu_inline" (typeAttrs vi.vtype)) && (not vi.vinline || vi.vstorage <> Extern))) (* Return true if 's' starts with the prefix 'p' *) From 8d08752bdb058fe33bfc6323c50e4cdd6d9a62ef Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Fri, 18 Nov 2022 15:59:51 +0100 Subject: [PATCH 13/15] add comments --- doc/cil.tex | 4 ++++ src/ciloptions.ml | 2 -- src/mergecil.ml | 12 ++++++++---- test/Makefile | 2 ++ 4 files changed, 14 insertions(+), 6 deletions(-) diff --git a/doc/cil.tex b/doc/cil.tex index 156010005..716fa240e 100644 --- a/doc/cil.tex +++ b/doc/cil.tex @@ -2106,6 +2106,10 @@ \subsection{Code that CIL won't compile} \subsection{Code that behaves differently under CIL} \begin{itemize} +\item Without optimizations GCC generally does not use ``inline'' functions. +With optimizations they might be inlined. CIL assumes optimization, and also +assumes that ``inline'' functions are always inlined. + \item GCC has a strange feature called ``extern inline''. Such a function can be defined twice: first with the ``extern inline'' specifier and the second time without it. If optimizations are turned off then the ``extern inline'' diff --git a/src/ciloptions.ml b/src/ciloptions.ml index ada3e1ef1..92b83eaa7 100644 --- a/src/ciloptions.ml +++ b/src/ciloptions.ml @@ -165,7 +165,6 @@ let options : (string * Arg.spec * string) list = "--strictcheck", Arg.Unit (fun _ -> Cilutil.doCheck := true; Cilutil.strictChecking := true), " Same as --check, but treats problems as errors not warnings."; - "", Arg.Unit (fun _ -> ()), ""; "--cstd", Arg.String (fun s -> Cil.cstd := Cil.cstd_of_string s), " Specify the c language standard. Choose between c90, c99, c11"; @@ -177,7 +176,6 @@ let options : (string * Arg.spec * string) list = " Try to merge definitions of inline functions. They can appear in multiple files and we would like them all to be the same. This can slow down the merger an order of magnitude."; - "", Arg.Unit (fun _ -> ()), ""; "--noPrintLn", Arg.Unit (fun _ -> diff --git a/src/mergecil.ml b/src/mergecil.ml index c00d9d614..2410a20eb 100644 --- a/src/mergecil.ml +++ b/src/mergecil.ml @@ -74,10 +74,14 @@ (* C99: inline functions are internal unless specified to be external GNU89: inline functions are external unless specified to be static or extern GNU89 inline semantics is used also when gnu_inline attribute is present on all inline declarations *) - let externallyVisible vi = vi.vstorage <> Static - && ((!Cil.cstd <> Cil.C90 && not !Cil.gnu89inline && (not vi.vinline || vi.vstorage = Extern)) - || ((!Cil.cstd == Cil.C90 || !Cil.gnu89inline || hasAttribute "gnu_inline" (typeAttrs vi.vtype)) - && (not vi.vinline || vi.vstorage <> Extern))) + let externallyVisible vi = + match vi.vstorage with + | Static -> false + | _ -> (match !Cil.cstd, !Cil.gnu89inline, hasAttribute "gnu_inline" (typeAttrs vi.vtype) with + | Cil.C90, _, _ + | _, true, _ + | _, _, true -> not vi.vinline || vi.vstorage <> Extern + | _, _, _ -> not vi.vinline || vi.vstorage = Extern) (* Return true if 's' starts with the prefix 'p' *) let prefix p s = diff --git a/test/Makefile b/test/Makefile index 67f0be6be..903d77519 100644 --- a/test/Makefile +++ b/test/Makefile @@ -303,6 +303,8 @@ arcombine: mustbegcc combinec99%: $(SMALL1)/combine-c99%_1.c +# With no optimization gcc does not inline functions in general -> without -O1 calls +# to inline functions (cilly always inlines) would cause an 'undefined reference error' cd $(SMALL1); \ $(CILLY) $(CFLAGS) -O1 -std=c99 --verbose -fcommon --merge \ $(notdir $(wildcard $(SMALL1)/combine-c99$*_[1-9].c)) \ From b117e7d68a96c7ee1244ae86457501d1a7a8bf9a Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Fri, 18 Nov 2022 16:38:15 +0100 Subject: [PATCH 14/15] make gnu89 inline test a merge test --- test/Makefile | 7 +++++++ test/small1/{combine23_1.c => combinemerge1_1.c} | 0 test/small1/{combine23_2.c => combinemerge1_2.c} | 0 test/small1/{combine23_3.c => combinemerge1_3.c} | 0 test/testcil.pl | 2 +- 5 files changed, 8 insertions(+), 1 deletion(-) rename test/small1/{combine23_1.c => combinemerge1_1.c} (100%) rename test/small1/{combine23_2.c => combinemerge1_2.c} (100%) rename test/small1/{combine23_3.c => combinemerge1_3.c} (100%) diff --git a/test/Makefile b/test/Makefile index 903d77519..27f09f2b8 100644 --- a/test/Makefile +++ b/test/Makefile @@ -287,6 +287,13 @@ combine%: $(SMALL1)/combine%_1.c $(EXEOUT)combine$*.exe cd $(SMALL1); ./combine$*.exe +combinemerge%: $(SMALL1)/combinemerge%_1.c + cd $(SMALL1); \ + $(CILLY) $(CFLAGS) -std=gnu90 -fcommon --merge\ + $(notdir $(wildcard $(SMALL1)/combinemerge$*_[1-9].c)) \ + $(EXEOUT)combinemerge$*.exe + cd $(SMALL1); ./combinemerge$*.exe + combinegnuinline: cd $(SMALL1); \ $(CILLY) --merge $(CFLAGS) -std=gnu90 -fcommon \ diff --git a/test/small1/combine23_1.c b/test/small1/combinemerge1_1.c similarity index 100% rename from test/small1/combine23_1.c rename to test/small1/combinemerge1_1.c diff --git a/test/small1/combine23_2.c b/test/small1/combinemerge1_2.c similarity index 100% rename from test/small1/combine23_2.c rename to test/small1/combinemerge1_2.c diff --git a/test/small1/combine23_3.c b/test/small1/combinemerge1_3.c similarity index 100% rename from test/small1/combine23_3.c rename to test/small1/combinemerge1_3.c diff --git a/test/testcil.pl b/test/testcil.pl index 55982ff42..08a8a526d 100644 --- a/test/testcil.pl +++ b/test/testcil.pl @@ -432,7 +432,6 @@ sub addToGroup { addTest("combine21 "); addTest("combine22 "); addBadComment("combine22", "Bug. Outstanding since 1.3.6 at least"); -addTest("combine23 "); addTest("combinealias "); addTest("combinelibrik "); addTest("combineenum1 "); @@ -447,6 +446,7 @@ sub addToGroup { addTest("combineinline4 "); addBadComment("combineinline4", "Bug. Outstanding since 1.3.6 at least"); addTest("combineinline6 "); +addTest("combinemerge1"); addTest("combinestruct1 "); addTest("mixedcomb "); addTest("testrun/math1 "); From f95a68907dd1cc103f92c63eda274c89b24f35b0 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Wed, 23 Nov 2022 14:12:06 +0100 Subject: [PATCH 15/15] fix the descriptions of options for printing --- lib/perl5/App/Cilly.pm.in | 4 ---- src/ciloptions.ml | 16 +++++++--------- src/main.ml | 4 ++-- 3 files changed, 9 insertions(+), 15 deletions(-) diff --git a/lib/perl5/App/Cilly.pm.in b/lib/perl5/App/Cilly.pm.in index 01cf7737e..9e7e91342 100644 --- a/lib/perl5/App/Cilly.pm.in +++ b/lib/perl5/App/Cilly.pm.in @@ -215,10 +215,6 @@ sub collectOneArgument { if($arg eq "--verbose") { $self->{VERBOSE} = 1; return 1; } - if($arg eq "--cstd=(.+)\$") { - push @{$self->{CILARGS}}, $1; - return 1; - } if($arg eq "--flatten_linker_scripts") { $self->{FLATTEN_LINKER_SCRIPTS} = 1; return 1; } diff --git a/src/ciloptions.ml b/src/ciloptions.ml index 92b83eaa7..ba119124c 100644 --- a/src/ciloptions.ml +++ b/src/ciloptions.ml @@ -170,12 +170,10 @@ let options : (string * Arg.spec * string) list = " Specify the c language standard. Choose between c90, c99, c11"; "--gnu89inline", Arg.Set Cil.gnu89inline, - "Use gnu89 semantic for inlining"; + " Use gnu89 semantic for inlining"; "--mergeinlines", Arg.Unit (fun _ -> Mergecil.merge_inlines := true), - " Try to merge definitions of inline functions. They can appear in multiple - files and we would like them all to be the same. This can slow down the - merger an order of magnitude."; + " Try to merge definitions of inline functions."; "--noPrintLn", Arg.Unit (fun _ -> @@ -193,7 +191,7 @@ let options : (string * Arg.spec * string) list = Arg.Unit (fun _ -> Cil.lineDirectiveStyle := Some Cil.LineCommentSparse; Cprint.printLnComment := true), - " Print commented #line directives in the output only when\n\t\t\t\tthe line number changes."; + " Print commented #line directives in the output only when the line number changes."; "--stats", Arg.Set Cilutil.printStats, @@ -243,7 +241,7 @@ let options : (string * Arg.spec * string) list = "--extrafiles", Arg.String parseExtraFile, - " File that contains a list of additional files to process,\n\t\t\t\tseparated by newlines"; + " File that contains a list of additional files to process, separated by newlines"; (* Lowering Options *) "", Arg.Unit (fun () -> ()), " \n\t\tLowering Options\n"; @@ -302,13 +300,13 @@ let options : (string * Arg.spec * string) list = "--useLogicalOperators", Arg.Set Cil.useLogicalOperators, - (" Where possible (that is, if there are no side-effects),\n\t\t\t\t" ^ + (" Where possible (that is, if there are no side-effects)," ^ "retain &&, || and ?: (instead of transforming them to If statements)" ^ is_default !Cil.useLogicalOperators); "--noUseLogicalOperators", Arg.Clear Cil.useLogicalOperators, - ("Transform &&, || and ?: to If statements" ^ + (" Transform &&, || and ?: to If statements" ^ is_default (not !Cil.useLogicalOperators)); "--useComputedGoto", @@ -361,7 +359,7 @@ let options : (string * Arg.spec * string) list = "--noPrintCilAsIs", Arg.Clear Cil.printCilAsIs, - (" Simplify the CIL when printing. This produces prettier output\n\t\t\t\tby e.g. changing while(1) into more meaningful loops " ^ is_default (not !Cil.printCilAsIs)); + (" Simplify the CIL when printing. This produces prettier output by e.g. changing while(1) into more meaningful loops" ^ is_default (not !Cil.printCilAsIs)); "--noWrap", Arg.Unit (fun _ -> Cil.lineLength := 100_000), diff --git a/src/main.ml b/src/main.ml index 4db24bf49..ffdcc4d15 100644 --- a/src/main.ml +++ b/src/main.ml @@ -169,10 +169,10 @@ let theMain () = [ "--out", Arg.String (openFile "output" (fun oc -> outChannel := Some oc)), - " the name of the output CIL file.\n\t\t\t\tThe cilly script sets this for you."; + " The name of the output CIL file. The cilly script sets this for you."; "--mergedout", Arg.String (openFile "merged output" (fun oc -> mergedChannel := Some oc)), - " specify the name of the merged file"; + " Specify the name of the merged file"; "--load", Arg.String ignore, "" (* ignore --load because they have been processed above already *) ] @ F.args @ featureArgs in