Merge branch 'feature/kernel/log-truncation' into 'master'

[kernel] Indicates message truncation, and only truncate messages on terminal.

Closes #1244

See merge request frama-c/frama-c!4911

nix/internal-tests.nix

@@ -54,6 +54,7 @@
 , perl
 , python3
 , python3Packages
+, socat
 , swi-prolog
 , time
 , unixtools
@@ -128,6 +129,7 @@ stdenvNoCC.mkDerivation rec {
     python3
     python3Packages.jsonschema
     python3Packages.pyaml
+    socat
     swi-prolog
     time
     unixtools.getopt

nix/mk_tests.nix

@@ -34,6 +34,7 @@
 , jq
 , perl
 , python3Packages
+, socat
 , stdenvNoCC
 , time
 , unixtools
@@ -65,6 +66,7 @@ stdenvNoCC.mkDerivation {
     perl
     python3Packages.jsonschema
     python3Packages.pyaml
+    socat
     time
     unixtools.getopt
     which

src/kernel_services/plugin_entry_points/log.ml

@@ -20,6 +20,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* Messages longer than N characters are truncated when printed on terminal. *)
+let max_message_length = 10000
+
 type kind = Result | Feedback | Debug | Warning | Error | Failure
 
 [@@@ warning "-32"]
@@ -467,6 +470,7 @@ let logtransient channel text =
        try
          Format.pp_print_newline fmt () ;
          Format.pp_print_flush fmt () ;
+         ignore (Rich_text.truncate buffer max_message_length) ;
          let p,q = Rich_text.trim buffer in
          do_transient channel.terminal (Rich_text.contents buffer) p q ;
          close_buffer channel
@@ -497,11 +501,19 @@ let logwithfinal finally channel
          Format.pp_close_box fmt () ;
          Format.pp_print_newline fmt () ;
          Format.pp_print_flush fmt () ;
+         let truncated =
+           if channel.terminal.isatty
+           then Rich_text.truncate buffer max_message_length
+           else false
+         in
          let p,q = Rich_text.trim buffer in
          let output =
            if p <= q then
              let source = get_source current source in
              let message = Rich_text.range buffer p q in
+             let message =
+               if truncated then "(truncated message) " ^ message else message
+             in
              let event = {
                evt_kind = kind ;
                evt_plugin = channel.plugin ;

src/libraries/utils/rich_text.ml

@@ -106,8 +106,6 @@ let pretty ?vbox fmt message =
 (* -------------------------------------------------------------------------- *)
 
 let min_buffer = 128    (* initial size of buffer *)
-let max_buffer = 2097152 (* maximal size of buffer *)
-let tgr_buffer = 3145728 (* elasticity (internal overhead) *)
 
 type buffer = {
   mutable formatter : Format.formatter ; (* formatter on self (recursive) *)
@@ -136,7 +134,8 @@ let shrink buffer =
   if Buffer.length buffer.content > min_buffer then
     Buffer.reset buffer.content
 
-let truncate_text buffer size =
+let truncate buffer size =
+  let truncated = ref false in
   if Buffer.length buffer.content > size then
     begin
       let p = trim_begin buffer in
@@ -147,23 +146,21 @@ let truncate_text buffer size =
       else if n <= size then
         Buffer.blit buffer.content p (Buffer.to_bytes buffer.content) 0 n
       else
-        begin
-          let n_left = size / 2 - 3 in
-          let n_right = size - n_left - 5 in
-          if p > 0 then
-            Buffer.blit buffer.content p (Buffer.to_bytes buffer.content) 0 n_left;
-          let buf_right = Buffer.sub buffer.content (q-n_right+1) n_right in
-          Buffer.truncate buffer.content n_left;
-          Buffer.add_string buffer.content "[...]";
-          Buffer.add_string buffer.content buf_right;
-        end
-    end
+        let n_left = size / 2 - 3 in
+        let n_right = size - n_left - 5 in
+        if p > 0 then
+          Buffer.blit buffer.content p (Buffer.to_bytes buffer.content) 0 n_left;
+        let buf_right = Buffer.sub buffer.content (q-n_right+1) n_right in
+        Buffer.truncate buffer.content n_left;
+        Buffer.add_string buffer.content "[...]";
+        Buffer.add_string buffer.content buf_right;
+        truncated := true;
+    end;
+  !truncated
 
 (* All text added shall go through this function *)
 let append buffer s k n =
-  Buffer.add_substring buffer.content s k n ;
-  if Buffer.length buffer.content > tgr_buffer then
-    truncate_text buffer max_buffer
+  Buffer.add_substring buffer.content s k n
 
 let push_tag buffer _tag =
   let p = Buffer.length buffer.content in
@@ -219,13 +216,12 @@ let create ?indent ?margin () =
   buffer
 
 let trim buffer =
-  truncate_text buffer max_buffer ;
   let p = trim_begin buffer in
   let q = trim_end buffer in
   p , q
 
 let contents buffer =
-  truncate_text buffer max_buffer ; Buffer.contents buffer.content
+  Buffer.contents buffer.content
 
 let message buffer =
   ( Buffer.contents buffer.content , List.rev buffer.revtags )
@@ -247,7 +243,6 @@ let to_string ?(indent=20) ?(margin=40) ?(trim=true) pp data =
   let fmt = formatter buffer in
   pp fmt data ;
   Format.pp_print_flush fmt () ;
-  truncate_text buffer max_buffer ;
   if trim then
     let p = trim_begin buffer in
     let q = trim_end buffer in

src/libraries/utils/rich_text.mli

@@ -106,6 +106,10 @@ val trim : buffer -> int * int
 (** Resize the buffer to roughly fit its actual content. *)
 val shrink : buffer -> unit
 
+(** [truncate buffer size] truncates the content of [buffer] if longer than
+    [size] characters. Returns true if the bufffer has been truncated. *)
+val truncate : buffer -> int -> bool
+
 (* -------------------------------------------------------------------------- *)
 (** Printer *)
 (* -------------------------------------------------------------------------- *)

tests/misc/dune

@@ -8,3 +8,8 @@
   (enabled_if %{bin-available:gcc})
   (deps pragma-pack.c pragma-pack-utils.h)
 )
+
+(cram
+  (applies_to log-truncation)
+  (enabled_if %{bin-available:socat})
+)

tests/misc/log-truncation.t/dune

+(executable
+  (name "log_truncation")
+  (modules "log_truncation")
+  (modes plugin)
+  (libraries frama-c.init.cmdline frama-c.kernel)
+  (flags -open Frama_c_kernel :standard)
+  (promote (until-clean))
+)

tests/misc/log-truncation.t/dune-project

+(lang dune 3.13)
+(name frama-c-log-truncation)
+(package (name frama-c-log-truncation))

tests/misc/log-truncation.t/log_truncation.ml

+let run () =
+  (* This can be filtered to avoid too long test oracles. *)
+  let very_long_line = String.make 5000 '#' in
+  let line = "begin_line <-----" ^ very_long_line ^ "-----> end_line" in
+  let middle_text =
+    "[ This text should only appear in the log if is is redirected to a file. ]"
+  in
+  Kernel.warning
+    "This is a very, very long message intended to test the truncation \
+     of the Frama-C log: \n\
+     @[<v>%s@;%s@;%s@]" line middle_text line
+
+let () = Boot.Main.extend run

tests/misc/log-truncation.t/run.t

+Compilation of the log_truncation.ml file.
+  $ dune build --cache=disabled --root . _build/default/log_truncation.cmxs
+
+  $ frama-c -no-autoload-plugins -load-module log_truncation.cmxs > file-log.txt
+
+The message should not be truncated as the output was redireted to a file.
+  $ cat file-log.txt | tr -d '#'
+  [kernel] Warning: This is a very, very long message intended to test the truncation of the Frama-C log: 
+    
+    begin_line <----------> end_line
+    [ This text should only appear in the log if is is redirected to a file. ]
+    begin_line <----------> end_line
+
+  $ socat EXEC:"frama-c -no-autoload-plugins -load-module log_truncation.cmxs",pty GOPEN:terminal-log.txt
+
+The message should be truncated.
+  $ cat terminal-log.txt | tr -d '#'
+  [kernel] Warning: (truncated message) This is a very, very long message intended to test the truncation of the Frama-C log: 
+    
+    begin_line <-----[...]-----> end_line