From: Gereon Kremer <nafur42@gmail.com>
Date: Mon, 24 Aug 2020 20:43:48 +0000 (+0200)
Subject: Fix memory issue in AntlrInput::parseError (#4873)
X-Git-Tag: cvc5-1.0.0~2959
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5852810e110a002ad9a3b04b929470a4b61abe98;p=cvc5.git

Fix memory issue in AntlrInput::parseError (#4873)

The `parseErrorHelper` message can run into memory errors when the it prints the last line and this last line is not terminated by a newline. I suspect other conditions may trigger it as well (like only using `\r` as line terminator).
This comit computes the size of the buffer from the start of the current line to the end of the buffer and makes sure that we never go beyond this buffer. The calculation looks a bit awkward, I've not been able to obtain this information from the ANTLR input stream in a nicer way...
(I found this issue when looking at #4866).
Fixes #4069 .
---

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 1d5190e3f..bf5e8824a 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -389,7 +389,10 @@ size_t wholeWordMatch(string input, string pattern, bool (*isWordChar)(char)) {
  *   found to be totally unhelpful. (TODO: fix this upstream to
  *   improve)
  */
-std::string parseErrorHelper(const char* lineStart, int charPositionInLine, const std::string& message)
+std::string parseErrorHelper(const char* lineStart,
+                             std::size_t lineLength,
+                             std::size_t charPositionInLine,
+                             const std::string& message)
 {
   // Is it a multi-line message
   bool multilineMessage = (message.find('\n') != string::npos);
@@ -405,17 +408,20 @@ std::string parseErrorHelper(const char* lineStart, int charPositionInLine, cons
     ss << message << endl << endl;
   }
 
-  int posSliceStart = (charPositionInLine - 50 <= 0) ? 0 : charPositionInLine - 50 + 5;
-  int posSliceEnd = posSliceStart + 70;
-  int caretPos = 0;
-  int caretPosExtra = 0; // for inital intendation, epilipses etc.
+  std::size_t posSliceStart =
+      (charPositionInLine <= 50) ? 0 : charPositionInLine - 50 + 5;
+  std::size_t posSliceEnd = posSliceStart + 70;
+  std::size_t caretPos = 0;
+  std::size_t caretPosExtra = 0;  // for inital intendation, epilipses etc.
 
   ss << "  "; caretPosExtra += 2;
   if(posSliceStart > 0) {
     ss << "..."; caretPosExtra += 3;
   }
 
-  for(int i = posSliceStart; lineStart[i] != '\n'; ++i) {
+  for (std::size_t i = posSliceStart; i < lineLength && lineStart[i] != '\n';
+       ++i)
+  {
     if(i == posSliceEnd) {
       ss << "...";
       break;
@@ -501,9 +507,14 @@ std::string parseErrorHelper(const char* lineStart, int charPositionInLine, cons
 
 void AntlrInput::parseError(const std::string& message, bool eofException)
 {
-  string updatedMessage = parseErrorHelper((const char*)d_antlr3InputStream->getLineBuf(d_antlr3InputStream),
-                                           d_lexer->getCharPositionInLine(d_lexer),
-                                           message);
+  auto lineLength = d_antlr3InputStream->sizeBuf
+                    - (static_cast<char*>(d_antlr3InputStream->currentLine)
+                       - static_cast<char*>(d_antlr3InputStream->data));
+  std::string updatedMessage = parseErrorHelper(
+      (const char*)d_antlr3InputStream->getLineBuf(d_antlr3InputStream),
+      lineLength,
+      d_lexer->getCharPositionInLine(d_lexer),
+      message);
 
   Debug("parser") << "Throwing exception: "
       << (const char*)d_lexer->rec->state->tokSource->fileName->chars << ":"