Merge pull request #89 from goblint/transform-location

sim642 · web-flow · commit faff341f1e8f · 2022-04-11T09:46:57.000+03:00
Allow parsed location directive transformation
diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml
@@ -46,3 +46,10 @@ jobs:
       - run: opam install . --deps-only --with-doc --with-test
       - run: opam exec -- dune build
       - run: opam exec -- dune runtest
+
+      - name: Upload test log
+        uses: actions/upload-artifact@v3
+        if: failure()
+        with:
+          name: ${{ matrix.os }}-${{ matrix.ocaml-version }}
+          path: _build/default/test/cil.log
diff --git a/src/cil.ml b/src/cil.ml
@@ -156,9 +156,6 @@ type file =
           should always be false if there is no global initializer. When
           you create a global initialization CIL will try to insert code in
           main to call it. *)
-      files: (string * bool) list;
-      (** A list of those files that were encountered during parsing of this CIL file,
-          and whether they are system header files  *)
     }
 
 and comment = location * string
@@ -5011,8 +5008,7 @@ let dummyFile =
   { globals = [];
     fileName = "<dummy>";
     globinit = None;
-    globinitcalled = false;
-    files = []; }
+    globinitcalled = false;}
 
 (***** Load and store files as unmarshalled Ocaml binary data. ****)
 type savedFile =
diff --git a/src/cil.mli b/src/cil.mli
@@ -93,9 +93,6 @@ type file =
        * create a global initialization CIL will try to insert code in main
        * to call it. This will not happen if your file does not contain a
        * function called "main" *)
-       files: (string * bool) list;
-       (** A list of those files that were encountered during parsing of this CIL file,
-        * and whether they are system header files *)
     }
 (** Top-level representation of a C source file *)
 
diff --git a/src/dune b/src/dune
@@ -4,7 +4,7 @@
   (public_name goblint-cil)
   (name cil)
   (wrapped false) ; this should be changed, but then module paths in goblint need to be prefixed
-  (libraries zarith findlib dynlink unix str stdlib-shims batteries.unthreaded)
+  (libraries zarith findlib dynlink unix str stdlib-shims batteries.unthreaded) ; batteries shouldn't be needed, but tests fail on MacOS otherwise: https://github.com/goblint/cil/pull/89#issuecomment-1092610041
   (modules (:standard \ main))
 )
 
diff --git a/src/formatcil.ml b/src/formatcil.ml
@@ -80,15 +80,15 @@ let doParse (prog: string)
       Formatparse.initialize Formatlex.initial lexbuf;
       let res = theParser Formatlex.initial lexbuf in
       H.add memoTable prog res;
-      ignore @@ Formatlex.finish ();
+      Formatlex.finish ();
       res
     with Parsing.Parse_error -> begin
-      ignore @@ Formatlex.finish ();
+      Formatlex.finish ();
       E.s (E.error "Parsing error: %s" prog)
     end
     | e -> begin
         ignore (E.log "Caught %s while parsing\n" (Printexc.to_string e));
-        ignore @@ Formatlex.finish ();
+        Formatlex.finish ();
         raise e
     end
   end
diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml
@@ -189,9 +189,8 @@ and definition =
  | STATIC_ASSERT of expression * string * cabsloc
 
 
-(* the string is a file name, then the list of toplevel forms, and finally a list of filenames
-   encountered during parsing and whether they are system headers *)
-and file = string * definition list * (string * bool) list
+(* the string is a file name, and then the list of toplevel forms *)
+and file = string * definition list
 
 
 (*
diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml
@@ -6897,7 +6897,7 @@ let convFile (f : A.file) : Cil.file =
   Cil.initCIL (); (* make sure we have initialized CIL *)
 
   (* remove parentheses from the Cabs *)
-  let fname,dl,files = stripParenFile f in
+  let fname,dl = stripParenFile f in
 
   (* Clean up the global types *)
   initGlobals();
@@ -6986,5 +6986,4 @@ let convFile (f : A.file) : Cil.file =
     globals  = !globals;
     globinit = None;
     globinitcalled = false;
-    files = files;
   }
diff --git a/src/frontc/cabsvisit.ml b/src/frontc/cabsvisit.ml
@@ -582,7 +582,7 @@ and childrenAttribute vis ((n, el) as input) =
 and visitCabsAttributes vis (al: attribute list) : attribute list =
   mapNoCopyList (visitCabsAttribute vis) al
 
-let visitCabsFile (vis: cabsVisitor) ((fname, f, files): file) : file =
-  (fname, mapNoCopyList (visitCabsDefinition vis) f, files)
+let visitCabsFile (vis: cabsVisitor) ((fname, f): file) : file =
+  (fname, mapNoCopyList (visitCabsDefinition vis) f)
 
     (* end of file *)
diff --git a/src/frontc/clexer.mli b/src/frontc/clexer.mli
@@ -43,8 +43,7 @@
 
 
 val init: filename:string -> Lexing.lexbuf
-val finish: unit -> (string * bool) list (* Return the list of filenames encountered during lexing
-                                            and whether they are system headers *)
+val finish: unit -> unit
 
 (* This is the main parser function *)
 val initial: Lexing.lexbuf -> Cparser.token
diff --git a/src/frontc/clexer.mll b/src/frontc/clexer.mll
@@ -659,9 +659,8 @@ and hash = parse
                    E.warn "Bad line number in preprocessed file: %s" s;
                    (-1)
                  in
-                  E.setCurrentLine (lineno - 1);
                   (* A file name may follow *)
-		  file lexbuf }
+		  file (lineno - 1) lexbuf }
 | "line"        { addWhite lexbuf; hash lexbuf } (* MSVC line number info *)
                 (* For pragmas with irregular syntax, like #pragma warning,
                  * we parse them as a whole line. *)
@@ -672,15 +671,15 @@ and hash = parse
 | "pragma"      { pragmaLine := true; PRAGMA (currentLoc ()) }
 | _	        { addWhite lexbuf; endline lexbuf}
 
-and file =  parse
-        '\n'		        {addWhite lexbuf; E.newline (); initial lexbuf}
-|	blank			{addWhite lexbuf; file lexbuf}
+and file lineno =  parse
+        '\n'		        {addWhite lexbuf; E.setCurrent ~file:None ~line:lineno; E.newline (); initial lexbuf}
+|	blank			{addWhite lexbuf; file lineno lexbuf}
 |	'"' ([^ '\012' '\t' '"']* as filename) '"' ((' ' ['1' -'4'])* as flags)
        { addWhite lexbuf;  (* '"' *)
-         E.setCurrentFile filename (String.contains flags '3');
+         E.setCurrent ~file:(Some (filename, String.contains flags '3')) ~line:lineno;
 				 endline lexbuf}
 
-|	_			{addWhite lexbuf; endline lexbuf}
+|	_			{addWhite lexbuf; E.setCurrent ~file:None ~line:lineno; endline lexbuf}
 
 and endline = parse
         '\n' 			{ addWhite lexbuf; E.newline (); initial lexbuf}
diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml
@@ -936,7 +936,7 @@ end
 (*  print abstrac_syntax -> ()
 **		Pretty printing the given abstract syntax program.
 *)
-let printFile (result : out_channel) ((fname, defs, _) : file) =
+let printFile (result : out_channel) ((fname, defs) : file) =
   Whitetrack.setOutput result;
   print_defs defs;
   Whitetrack.printEOF ();
diff --git a/src/frontc/frontc.ml b/src/frontc/frontc.ml
@@ -188,31 +188,31 @@ and parse_to_cabs_inner (fname : string) =
     let lexbuf = Clexer.init ~filename:fname in
     let cabs = Stats.time "parse" (Cparser.interpret (Whitetrack.wraplexer clexer)) lexbuf in
     Whitetrack.setFinalWhite (Clexer.get_white ());
-    let files = Clexer.finish () in
-    (fname, cabs, files)
+    Clexer.finish ();
+    (fname, cabs)
   with (Sys_error msg) -> begin
     ignore (E.log "Cannot open %s : %s\n" fname msg);
-    ignore @@ Clexer.finish ();
+    Clexer.finish ();
     close_output ();
     raise (ParseError("Cannot open " ^ fname ^ ": " ^ msg ^ "\n"))
   end
   | Parsing.Parse_error -> begin
       ignore (E.log "Parsing error");
-      ignore @@ Clexer.finish ();
+      Clexer.finish ();
       close_output ();
       (* raise (ParseError("Parse error")) *)
       let backtrace = Printexc.get_raw_backtrace () in
       Printexc.raise_with_backtrace (ParseError("Parse error")) backtrace (* re-raise with captured inner backtrace *)
   end
   | e -> begin
       ignore (E.log "Caught %s while parsing\n" (Printexc.to_string e));
-      ignore @@ Clexer.finish ();
+      Clexer.finish ();
       raise e
   end
 
 
 (* print to safec.proto.h the prototypes of all functions that are defined *)
-let printPrototypes ((fname, file, _) : Cabs.file) : unit =
+let printPrototypes ((fname, file) : Cabs.file) : unit =
 begin
   (*ignore (E.log "file has %d defns\n" (List.length file));*)
 
diff --git a/src/frontc/patch.ml b/src/frontc/patch.ml
@@ -333,8 +333,9 @@ let gettime () : float =
 
 let rec applyPatch (patchFile : file) (srcFile : file) : file =
 begin
-  let (_, patch, _) = patchFile in
-  let (srcFname, src, srcFiles) = srcFile in
+  let patch : definition list = (snd patchFile) in
+  let srcFname : string = (fst srcFile) in
+  let src : definition list = (snd srcFile) in
 
   (trace "patchTime" (dprintf "applyPatch start: %f\n" (gettime ())));
   if (traceActive "patchDebug") then
@@ -416,7 +417,7 @@ begin
   );
 
   (trace "patchTime" (dprintf "applyPatch finish: %f\n" (gettime ())));
-  (srcFname, result, srcFiles)
+  (srcFname, result)
 end
 
 
diff --git a/src/mergecil.ml b/src/mergecil.ml
@@ -1675,11 +1675,6 @@
        incr currentFidx)
      files;
 
-   let filesH = Hashtbl.create 50 in
-   List.iter
-     (fun f -> List.iter (fun f -> Hashtbl.replace filesH f ()) f.files)
-     files;
-
    (* Now reverse the result and return the resulting file *)
    let rec revonto acc = function [] -> acc | x :: t -> revonto (x :: acc) t in
    let res =
@@ -1688,8 +1683,6 @@
        globals = revonto (revonto [] !theFile) !theFileTypes;
        globinit = None;
        globinitcalled = false;
-       files =
-         Hashtbl.fold (fun k v acc -> k :: acc) filesH [] (* keys are unique *);
      }
    in
    init ();
diff --git a/src/ocamlutil/errormsg.ml b/src/ocamlutil/errormsg.ml
@@ -170,8 +170,7 @@ let theLexbuf = ref (Lexing.from_string "")
 let fail format = Pretty.gprintf (fun x -> Pretty.fprint stderr ~width:80 x;
                                            raise (Failure "")) format
 
-(***** Keep track of encountered files ******)
-let files = Hashtbl.create 10
+
 
 (***** Handling parsing errors ********)
 type parseinfo =
@@ -257,7 +256,6 @@ let startParsing ?(useBasename=true) (fname: string) =
       num_errors = 0 } in
 
   current := i;
-  Hashtbl.clear files;
   lexbuf
 
 let startParsingFromString ?(file="<string>") ?(line=1) (str: string) =
@@ -271,15 +269,12 @@ let startParsingFromString ?(file="<string>") ?(line=1) (str: string) =
       num_errors = 0 }
   in
   current := i;
-  Hashtbl.clear files;
   lexbuf
 
 let finishParsing () =
   let i = !current in
   (match i.inchan with Some c -> close_in c | _ -> ());
-  current := dummyinfo;
-  (* keys are unique *)
-  Hashtbl.fold (fun k v acc -> (k,v)::acc) files []
+  current := dummyinfo
 
 
 (* Call this function to announce a new line *)
@@ -292,13 +287,19 @@ let newHline () =
   let i = !current in
   i.hline <- 1 + i.hline
 
-let setCurrentLine (i: int) =
-  !current.linenum <- i
-
-let setCurrentFile (n: string) (system_header: bool) =
-  let cn = cleanFileName n in
-  Hashtbl.replace files cn system_header;
-  !current.fileName <- cn
+let transformLocation = ref (fun ~file ~line -> Some (file, line))
+
+let setCurrent ~file ~line =
+  match !transformLocation ~file ~line with
+  | Some (file, line) ->
+    begin match file with
+      | Some (n, system_header) ->
+        let cn = cleanFileName n in
+        !current.fileName <- cn
+      | None -> ()
+    end;
+    !current.linenum <- line
+  | None -> ()
 
 
 let max_errors = 20  (* Stop after 20 errors *)
diff --git a/src/ocamlutil/errormsg.mli b/src/ocamlutil/errormsg.mli
@@ -134,8 +134,8 @@ val getHPosition: unit -> int * string (** high-level position *)
 val setHLine: int -> unit
 val setHFile: string -> unit
 
-val setCurrentLine: int -> unit
-val setCurrentFile: string -> bool -> unit
+val transformLocation: (file:(string * bool) option -> line:int -> ((string * bool) option * int) option) ref
+val setCurrent: file:(string * bool) option -> line:int -> unit
 
 (** Type for source-file locations *)
 type location =
@@ -170,6 +170,7 @@ val startParsing:  ?useBasename:bool -> string ->
 val startParsingFromString: ?file:string -> ?line:int -> string
                             -> Lexing.lexbuf
 
-val finishParsing: unit -> (string * bool) list (* Call this function to finish parsing and
-                                        * close the input channel, returns a list of all
-                                        * encountered filenames and whether they are system headers *)
+val finishParsing: unit -> unit (* Call this function to finish parsing and 
+                                 * close the input channel *)
+
+

Original file line number	Diff line number	Diff line change
`@@ -93,9 +93,6 @@ type file =`
`93`	`93`	`* create a global initialization CIL will try to insert code in main`
`94`	`94`	`* to call it. This will not happen if your file does not contain a`
`95`	`95`	`* function called "main" *)`
`96`		`- files: (string * bool) list;`
`97`		`- (** A list of those files that were encountered during parsing of this CIL file,`
`98`		`- * and whether they are system header files *)`
`99`	`96`	`}`
`100`	`97`	`(** Top-level representation of a C source file *)`
`101`	`98`
Original file line number	Diff line number	Diff line change
`@@ -4,7 +4,7 @@`
`4`	`4`	`(public_name goblint-cil)`
`5`	`5`	`(name cil)`
`6`	`6`	`(wrapped false) ; this should be changed, but then module paths in goblint need to be prefixed`
`7`		`- (libraries zarith findlib dynlink unix str stdlib-shims batteries.unthreaded)`
	`7`	`+ (libraries zarith findlib dynlink unix str stdlib-shims batteries.unthreaded) ; batteries shouldn't be needed, but tests fail on MacOS otherwise: https://github.com/goblint/cil/pull/89#issuecomment-1092610041`
`8`	`8`	`(modules (:standard \ main))`
`9`	`9`	`)`
`10`	`10`