From 938a44c4797e7d6a8545b23c19e1fbcc81b9e1b8 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 16 Nov 2021 15:53:12 +0100
Subject: [PATCH] [eacsl] Add `rtl_snprintf` function and replace uses of
 `rtl_sprintf` where possible

---
 .../e-acsl/internals/e_acsl_private_assert.c  |  10 +-
 .../share/e-acsl/internals/e_acsl_rtl_io.c    | 161 +++++++++++++-----
 .../share/e-acsl/internals/e_acsl_rtl_io.h    |   9 +
 .../share/e-acsl/internals/e_acsl_trace.c     |   6 +-
 .../segment_model/e_acsl_segment_tracking.c   |  20 +--
 .../segment_model/e_acsl_segment_tracking.h   |   2 +-
 6 files changed, 141 insertions(+), 67 deletions(-)

diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c
index 40da9b3985b..b4ca88e1fe5 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_private_assert.c
@@ -31,14 +31,6 @@
 
 #include "e_acsl_private_assert.h"
 
-#define prepend_file_line(file, line, fmt)                                     \
-  do {                                                                         \
-    char *afmt = "%s:%d: %s\n";                                                \
-    char buf[strlen(fmt) + strlen(afmt) + PATH_MAX + 11];                      \
-    rtl_sprintf(buf, afmt, file, line, fmt);                                   \
-    fmt = buf;                                                                 \
-  } while (0)
-
 void raise_abort(const char *file, int line) {
 #ifdef E_ACSL_DEBUG
 #  ifndef E_ACSL_NO_TRACE
@@ -69,7 +61,7 @@ void private_assert_fail(int expr, const char *file, int line, char *fmt, ...) {
   if (!expr) {
     char *afmt = "%s:%d: %s";
     char buf[strlen(fmt) + strlen(afmt) + PATH_MAX + 11];
-    rtl_sprintf(buf, afmt, file, line, fmt);
+    rtl_snprintf(buf, sizeof(buf), afmt, file, line, fmt);
     fmt = buf;
 
     va_list va;
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c
index 6bcc5370058..45bfaacbd04 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c
@@ -47,7 +47,26 @@
 
 #include "e_acsl_rtl_io.h"
 
-typedef void (*putcf)(void *, char);
+/*! \brief Test if we can still write `n + 1` characters to the buffer according
+    to the `count` variable. */
+#define TEST_COUNT_N(count, n) ((count) == NULL || *(count) > (n))
+
+/*! \brief Test if we can still write a character to the buffer according to
+    the `count` variable. */
+#define TEST_COUNT(count) TEST_COUNT_N(count, 0)
+
+/*! \brief Decrease the value of `*count` by `n` if `count` is not `NULL`. */
+#define DEC_COUNT_N(count, n)                                                  \
+  do {                                                                         \
+    if ((count) != NULL) {                                                     \
+      *(count) -= (n);                                                         \
+    }                                                                          \
+  } while (0)
+
+/*! \brief Decrease the value of `*count` by 1 if `count` is not `NULL`. */
+#define DEC_COUNT(count) DEC_COUNT_N(count, 1)
+
+typedef void (*putcf)(void *, size_t *, char);
 
 /* Unsigned long integers to string conversion (%u) */
 static void uli2a(unsigned long int num, unsigned int base, int uc, char *bf) {
@@ -209,28 +228,43 @@ static char a2i(char ch, char **src, int base, int *nump) {
   return ch;
 }
 
-static void putchw(void *putp, putcf putf, int n, char z, char *bf) {
+static void putchw(void *putp, size_t *count, putcf putf, int n, char z,
+                   char *bf) {
   char fc = z ? '0' : ' ';
   char ch;
   char *p = bf;
   while (*p++ && n > 0)
     n--;
   while (n-- > 0)
-    putf(putp, fc);
+    putf(putp, count, fc);
   while ((ch = *bf++))
-    putf(putp, ch);
+    putf(putp, count, ch);
 }
 
-static void putcp(void *p, char c) {
-  *(*((char **)p))++ = c;
+static void putcp(void *p, size_t *count, char c) {
+  if (TEST_COUNT(count)) {
+    *(*((char **)p))++ = c;
+    DEC_COUNT(count);
+  }
 }
 
-static void _format(void *putp, putcf putf, char *fmt, va_list va) {
+/** Load the data from the format string `fmt` and the variadic arguments `va`,
+ * convert them to character string equivalents and write the result to the
+ * stream `putp` with the function `putf` up to `count` characters.
+ * \param putp Pointer to a stream where the formatted string will be outputted.
+ * \param count Pointer to an integer representing the number of characters that
+ *        can still be written to `putp`, or `NULL` if there are no limits.
+ * \param putf Function pointer to write a character to a given stream.
+ * \param fmt Formatting string.
+ * \param va Arguments for the formatting string.
+ */
+static void _format(void *putp, size_t *count, putcf putf, char *fmt,
+                    va_list va) {
   char bf[256];
   char ch;
-  while ((ch = *(fmt++))) {
+  while ((ch = *(fmt++)) && TEST_COUNT(count)) {
     if (ch != '%') // if not '%' print character as is
-      putf(putp, ch);
+      putf(putp, count, ch);
     else { // otherwise do the print based on the format following '%'
       char lz = 0;
       char lng = 0; // long (i.e., 'l' specifier)
@@ -255,7 +289,7 @@ static void _format(void *putp, putcf putf, char *fmt, va_list va) {
           uli2a(va_arg(va, unsigned long int), 10, 0, bf);
         else
           ui2a(va_arg(va, unsigned int), 10, 0, bf);
-        putchw(putp, putf, w, lz, bf);
+        putchw(putp, count, putf, w, lz, bf);
         break;
       }
       case 'd': {
@@ -263,32 +297,32 @@ static void _format(void *putp, putcf putf, char *fmt, va_list va) {
           li2a(va_arg(va, unsigned long int), bf);
         else
           i2a(va_arg(va, int), bf);
-        putchw(putp, putf, w, lz, bf);
+        putchw(putp, count, putf, w, lz, bf);
         break;
       }
       case 'p':
         ptr2a(va_arg(va, void *), bf);
-        putchw(putp, putf, w, lz, bf);
+        putchw(putp, count, putf, w, lz, bf);
         break;
       case 'a':
         addr2a(va_arg(va, uintptr_t), bf);
-        putchw(putp, putf, w, lz, bf);
+        putchw(putp, count, putf, w, lz, bf);
         break;
       case 'b':
         bits2a(va_arg(va, long), w > 64 ? 64 : w ? w : 8, bf, 1);
-        putchw(putp, putf, 0, 0, bf);
+        putchw(putp, count, putf, 0, 0, bf);
         break;
       case 'B':
         bits2a(va_arg(va, long), w > 64 ? 64 : w ? w : 8, bf, 0);
-        putchw(putp, putf, 0, 0, bf);
+        putchw(putp, count, putf, 0, 0, bf);
         break;
       case 'v':
         pbits2a(va_arg(va, void *), w ? w : 8, bf, 1);
-        putchw(putp, putf, 0, 0, bf);
+        putchw(putp, count, putf, 0, 0, bf);
         break;
       case 'V':
         pbits2a(va_arg(va, void *), w ? w : 8, bf, 0);
-        putchw(putp, putf, 0, 0, bf);
+        putchw(putp, count, putf, 0, 0, bf);
         break;
       case 'x':
       case 'X':
@@ -296,29 +330,29 @@ static void _format(void *putp, putcf putf, char *fmt, va_list va) {
           uli2a(va_arg(va, unsigned long int), 16, (ch == 'X'), bf);
         else
           ui2a(va_arg(va, unsigned int), 16, (ch == 'X'), bf);
-        putchw(putp, putf, w, lz, bf);
+        putchw(putp, count, putf, w, lz, bf);
         break;
       case 'f': {
         double num = va_arg(va, double);
         int ord = (int)num;
         i2a(ord, bf);
-        putchw(putp, putf, w, lz, bf);
-        putf(putp, '.');
+        putchw(putp, count, putf, w, lz, bf);
+        putf(putp, count, '.');
         num = num - ord;
         num *= 1000;
         ord = (int)num;
         i2a(ord, bf);
-        putchw(putp, putf, w, lz, bf);
+        putchw(putp, count, putf, w, lz, bf);
         break;
       }
       case 'c':
-        putf(putp, (char)(va_arg(va, int)));
+        putf(putp, count, (char)(va_arg(va, int)));
         break;
       case 's':
-        putchw(putp, putf, w, 0, va_arg(va, char *));
+        putchw(putp, count, putf, w, 0, va_arg(va, char *));
         break;
       case '%':
-        putf(putp, ch);
+        putf(putp, count, ch);
       default:
         break;
       }
@@ -326,41 +360,58 @@ static void _format(void *putp, putcf putf, char *fmt, va_list va) {
   }
 }
 
-static void _charc_stdout(void *p, char c) {
-  write(STDOUT_FILENO, &c, 1);
+static void _charc_stdout(void *p, size_t *count, char c) {
+  if (TEST_COUNT(count)) {
+    write(STDOUT_FILENO, &c, 1);
+    DEC_COUNT(count);
+  }
 }
-static void _charc_stderr(void *p, char c) {
-  write(STDERR_FILENO, &c, 1);
+static void _charc_stderr(void *p, size_t *count, char c) {
+  if (TEST_COUNT(count)) {
+    write(STDERR_FILENO, &c, 1);
+    DEC_COUNT(count);
+  }
 }
-static void _charc_file(void *p, char c) {
-  write((size_t)p, &c, 1);
+static void _charc_file(void *p, size_t *count, char c) {
+  if (TEST_COUNT(count)) {
+    write((size_t)p, &c, 1);
+    DEC_COUNT(count);
+  }
 }
 
-static void _charc_literal(void *p, char c) {
+static void _charc_literal(void *p, size_t *count, char c) {
+#define CHARC_LITERAL_WRITE(s, n)                                              \
+  do {                                                                         \
+    if (TEST_COUNT_N(count, (n)-1)) {                                          \
+      write((size_t)p, s, n);                                                  \
+      DEC_COUNT_N(count, n);                                                   \
+    }                                                                          \
+  } while (0)
+
   switch (c) {
   case '\r':
-    write((size_t)p, "\\r", 2);
+    CHARC_LITERAL_WRITE("\\r", 2);
     break;
   case '\f':
-    write((size_t)p, "\\f", 2);
+    CHARC_LITERAL_WRITE("\\f", 2);
     break;
   case '\b':
-    write((size_t)p, "\\b", 2);
+    CHARC_LITERAL_WRITE("\\b", 2);
     break;
   case '\a':
-    write((size_t)p, "\\a", 2);
+    CHARC_LITERAL_WRITE("\\a", 2);
     break;
   case '\n':
-    write((size_t)p, "\\n", 2);
+    CHARC_LITERAL_WRITE("\\n", 2);
     break;
   case '\t':
-    write((size_t)p, "\\t", 2);
+    CHARC_LITERAL_WRITE("\\t", 2);
     break;
   case '\0':
-    write((size_t)p, "\\0", 2);
+    CHARC_LITERAL_WRITE("\\0", 2);
     break;
   default:
-    write((size_t)p, &c, 1);
+    CHARC_LITERAL_WRITE(&c, 1);
   }
 }
 
@@ -373,7 +424,7 @@ int rtl_printf(char *fmt, ...) {
 }
 
 int rtl_vprintf(char *fmt, va_list vlist) {
-  _format(NULL, _charc_stdout, fmt, vlist);
+  _format(NULL, NULL, _charc_stdout, fmt, vlist);
   return 1;
 }
 
@@ -386,7 +437,7 @@ int rtl_eprintf(char *fmt, ...) {
 }
 
 int rtl_veprintf(char *fmt, va_list vlist) {
-  _format(NULL, _charc_stderr, fmt, vlist);
+  _format(NULL, NULL, _charc_stderr, fmt, vlist);
   return 1;
 }
 
@@ -400,7 +451,7 @@ int rtl_dprintf(int fd, char *fmt, ...) {
 
 int rtl_vdprintf(int fd, char *fmt, va_list vlist) {
   intptr_t fd_long = fd;
-  _format((void *)fd_long, _charc_file, fmt, vlist);
+  _format((void *)fd_long, NULL, _charc_file, fmt, vlist);
   return 1;
 }
 
@@ -413,7 +464,29 @@ int rtl_sprintf(char *s, char *fmt, ...) {
 }
 
 int rtl_vsprintf(char *s, char *fmt, va_list vlist) {
-  _format(&s, putcp, fmt, vlist);
-  putcp(&s, 0);
+  _format(&s, NULL, putcp, fmt, vlist);
+  putcp(&s, NULL, 0);
+  return 1;
+}
+
+int rtl_snprintf(char *s, size_t bufsize, char *fmt, ...) {
+  va_list va;
+  va_start(va, fmt);
+  int result = rtl_vsnprintf(s, bufsize, fmt, va);
+  va_end(va);
+  return result;
+}
+
+int rtl_vsnprintf(char *s, size_t bufsize, char *fmt, va_list vlist) {
+  if (bufsize > 0) {
+    if (bufsize > 1) {
+      // Only copy `bufsize - 1` characters
+      --bufsize;
+      _format(&s, &bufsize, putcp, fmt, vlist);
+      ++bufsize;
+    }
+    // In any case, put `\0` as the last written character
+    putcp(&s, &bufsize, 0);
+  }
   return 1;
 }
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.h
index e5b93e73ca1..f26a145efd2 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.h
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.h
@@ -85,6 +85,15 @@ int rtl_vprintf(char *fmt, va_list vlist);
 int rtl_sprintf(char *s, char *fmt, ...);
 int rtl_vsprintf(char *s, char *fmt, va_list vlist);
 
+/* Same as sprintf buf write only up to ̀bufsize - 1` characters in the buffer
+   and the last character is always a `\0`.
+   This function is more secure than `sprintf()` because if the buffer `s` is
+   valid for `bufsize` characters, it guarantees that there will not be an out
+   of bound write. This function is used for instance in `private_assert_fail()`
+   or in `rtl_strerror()`. */
+int rtl_snprintf(char *s, size_t bufsize, char *fmt, ...);
+int rtl_vsnprintf(char *s, size_t bufsize, char *fmt, va_list vlist);
+
 /* Same as printf but write to the error stream. */
 int rtl_eprintf(char *fmt, ...);
 int rtl_veprintf(char *fmt, va_list vlist);
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
index 758debdc384..60888729cb2 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
@@ -83,13 +83,13 @@ void trace() {
   native_backtrace(bb, size);
 
   char executable[PATH_MAX];
-  rtl_sprintf(executable, "/proc/%d/exe", getpid());
+  rtl_snprintf(executable, sizeof(executable), "/proc/%d/exe", getpid());
 
   STDERR("/** Backtrace **************************/\n");
   int counter = 0;
   while (*bb) {
-    char *addr = (char *)private_malloc(21);
-    rtl_sprintf(addr, "%p", *bb);
+    char addr[21];
+    rtl_snprintf(addr, sizeof(addr), "%p", *bb);
     char *ar[] = {"addr2line", "-f",       "-p", "-C", "-s",
                   "-e",        executable, addr, NULL};
     ipr_t *ipr = shexec(ar, NULL);
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
index d2d45a9e820..6607555517d 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
@@ -1020,15 +1020,15 @@ void initialize_heap_region(uintptr_t addr, long len) {
 
 /* Internal state print (debug mode) {{{ */
 #ifdef E_ACSL_DEBUG
-void printbyte(unsigned char c, char buf[]) {
+void printbyte(unsigned char c, char buf[], size_t bufsize) {
   if (c >> 2 < LONG_BLOCK_INDEX_START) {
-    rtl_sprintf(buf, "PRIMARY: I{%u} RO{%u} OF{%2u} => %u[%u]",
-                checkbit(INIT_BIT, c), checkbit(READONLY_BIT, c), c >> 2,
-                short_lengths[c >> 2], short_offsets[c >> 2]);
+    rtl_snprintf(buf, bufsize, "PRIMARY: I{%u} RO{%u} OF{%2u} => %u[%u]",
+                 checkbit(INIT_BIT, c), checkbit(READONLY_BIT, c), c >> 2,
+                 short_lengths[c >> 2], short_offsets[c >> 2]);
   } else {
-    rtl_sprintf(buf, "SECONDARY:  I{%u} RO{%u} OF{%u} => %4u",
-                checkbit(INIT_BIT, c), checkbit(READONLY_BIT, c), (c >> 2),
-                (c >> 2) - LONG_BLOCK_INDEX_START);
+    rtl_snprintf(buf, bufsize, "SECONDARY:  I{%u} RO{%u} OF{%u} => %4u",
+                 checkbit(INIT_BIT, c), checkbit(READONLY_BIT, c), (c >> 2),
+                 (c >> 2) - LONG_BLOCK_INDEX_START);
   }
 }
 
@@ -1042,12 +1042,12 @@ void print_static_shadows(uintptr_t addr, size_t size) {
   int i, j = 0;
   for (i = 0; i < size; i++) {
     sec_buf[0] = '\0';
-    printbyte(prim_shadow[i], prim_buf);
+    printbyte(prim_shadow[i], prim_buf, sizeof(prim_buf));
     if (IS_LONG_BLOCK(size) && (i % LONG_BLOCK) == 0) {
       j += 2;
       if (i < LONG_BLOCK_BOUNDARY(size)) {
-        rtl_sprintf(sec_buf, " %a  SZ{%u} OF{%u}", &sec_shadow[j],
-                    sec_shadow[j - 2], sec_shadow[j - 1]);
+        rtl_snprintf(sec_buf, sizeof(sec_buf), " %a  SZ{%u} OF{%u}",
+                     &sec_shadow[j], sec_shadow[j - 2], sec_shadow[j - 1]);
       }
       if (i) {
         DLOG("---------------------------------------------\n");
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
index 15d70d047f0..6f2c8cc80a9 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
@@ -483,7 +483,7 @@ void initialize_heap_region(uintptr_t addr, long len);
 #ifdef E_ACSL_DEBUG
 /* ! \brief Print human-readable representation of a byte in a primary
  * shadow */
-void printbyte(unsigned char c, char buf[]);
+void printbyte(unsigned char c, char buf[], size_t bufsize);
 
 /*! \brief Print human-readable (well, ish) representation of a memory block
  * using primary and secondary shadows. */
-- 
GitLab