From 03f39523094fd41c8aad5ee7a8169ffc448cfd4a Mon Sep 17 00:00:00 2001
From: François Pottier <francois.pottier@inria.fr>
Date: Fri, 16 Oct 2015 17:56:06 +0200
Subject: Read the whole source C file into memory instad of reading it on
 demand. Having the file in memory will help build an error message. Also,
 this may be slightly faster.

---
 cparser/Lexer.mll |  4 ++--
 cparser/Parse.ml  | 18 +++++++++++++++---
 2 files changed, 17 insertions(+), 5 deletions(-)

(limited to 'cparser')

diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index 6be59aa8..aca1be27 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -440,7 +440,7 @@ and singleline_comment = parse
   open Parser
   open Aut.GramDefs
 
-  let tokens_stream filename channel : token coq_Stream =
+  let tokens_stream filename text : token coq_Stream =
     let tokens = Queue.create () in
     let lexer_wraper lexbuf : Pre_parser.token =
       let res =
@@ -452,7 +452,7 @@ and singleline_comment = parse
       Queue.push res tokens;
       res
     in
-    let lexbuf = Lexing.from_channel channel in
+    let lexbuf = Lexing.from_string text in
     lexbuf.lex_curr_p <- {lexbuf.lex_curr_p with pos_fname = filename; pos_lnum = 1};
     contexts_stk := [init_ctx];
     Pre_parser.translation_unit_file lexer_wraper lexbuf;
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index cfa95688..1d92d5a5 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -38,9 +38,22 @@ let parse_transformations s =
     s;
   !t
 
+let read_file sourcefile =
+  let ic = open_in sourcefile in
+  let n = in_channel_length ic in
+  let text = really_input_string ic n in
+  close_in ic;
+  text
+
 let preprocessed_file transfs name sourcefile =
   Cerrors.reset();
-  let ic = open_in sourcefile in
+  (* Reading the whole file at once may seem costly, but seems to be
+     the simplest / most robust way of accessing the text underlying
+     a range of positions. This is used when printing an error message.
+     Plus, I note that reading the whole file into memory leads to a
+     speed increase: "make -C test" speeds up by 3 seconds out of 40
+     on my machine. *)
+  let text = read_file sourcefile in
   let p =
     try
       let t = parse_transformations transfs in
@@ -52,7 +65,7 @@ let preprocessed_file transfs name sourcefile =
                  parsing of the entire file. This is non-negligeabe,
                  so we cannot use Timing.time2 *)
               (fun () ->
-                Parser.translation_unit_file inf (Lexer.tokens_stream name ic)) ()
+                Parser.translation_unit_file inf (Lexer.tokens_stream name text)) ()
            with
              | Parser.Parser.Inter.Fail_pr ->
                  (* Theoretically impossible : implies inconsistencies
@@ -65,5 +78,4 @@ let preprocessed_file transfs name sourcefile =
     with
     | Cerrors.Abort ->
         [] in
-  close_in ic;
   if Cerrors.check_errors() then None else Some p
-- 
cgit