Fix merging and renaming of inlines

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

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''
@@ -2357,7 +2361,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 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

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 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.
@@ -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}}, "--cstd", "c90";
+            }},
+      "-std=(c90|c89|iso9899:1990|iso9899:199409|gnu90|gnu89)" => {
+            TYPE => 'ALLARGS',
+            RUN => sub {
+                push @{$stub->{CILARGS}}, "--cstd", "c90";
+            }},
+      "-std=(c99|c9x|iso9899:1999|iso9899:199x|gnu99|gnu9x)" => {
+            TYPE => 'ALLARGS',
+            RUN => sub {
+                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}}, "--cstd", "c11";
+            }},
+      "-fgnu89-inline" => {
+            RUN => sub {
+                push @{$stub->{CILARGS}}, "--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

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",

src/cil.ml

@@ -55,11 +55,15 @@ 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.
+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):
@@ -2775,7 +2779,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
@@ -4298,13 +4302,10 @@ 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
-(*
-    | "used", [] when not !msvcMode -> text "__attribute_used__", false
-*)
     | "volatile", [] -> text "volatile", false
     | "restrict", [] -> text "__restrict", false
     | "missingproto", [] -> text "/* missing proto */", false

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
@@ -2021,10 +2026,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
 

src/ciloptions.ml

@@ -6,7 +6,7 @@
     Wes Weimer          <[email protected]>
     Ben Liblit          <[email protected]>
    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";
 
@@ -165,7 +165,17 @@ 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";
+
+    "--gnu89inline", Arg.Set Cil.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
+                      files and we would like them all to be the same. This can slow down the
+                      merger an order of magnitude.";
 
     "--noPrintLn",
     Arg.Unit (fun _ ->
@@ -179,7 +189,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 +214,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 ->

src/cilutil.ml

@@ -1,11 +1,11 @@
 (*
 
-   Copyright (c) 2001-2002, 
+   Copyright (c) 2001-2002,
     George C. Necula    <[email protected]>
     Scott McPeak        <[email protected]>
     Wes Weimer          <[email protected]>
    All rights reserved.
-   
+
    Redistribution and use in source and binary forms, with or without
    modification, are permitted provided that the following conditions are
    met:

src/mergecil.ml

@@ -71,6 +71,18 @@
     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 =
+  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 =
    let lp = String.length p in
@@ -809,7 +821,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 +853,7 @@
            currentLoc := l;
            incr currentDeclIdx;
            vi.vreferenced <- false;
-           if vi.vstorage <> Static then matchVarinfo vi (l, !currentDeclIdx)
+           if externallyVisible vi then matchVarinfo vi (l, !currentDeclIdx)
        | GFun (fdec, l) ->
            currentLoc := l;
            incr currentDeclIdx;
@@ -851,14 +863,8 @@
              (!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
+           if externallyVisible fdec.svar 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 +1340,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 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 *)
          let newName, _ = A.newAlphaName ~alphaTable:vtAlpha ~undolist:None ~lookupname:vi.vname ~data:!currentLoc in