From e1ac1e16c152f334e80061d01da7714572532ae0 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 21 Jun 2022 13:43:54 +0200
Subject: [PATCH] [kernel] break ill-formed recursion between bitsSizeOf et
 constfold

store normalized expressions for the arrays' size in the TypSize cache, so that we don't end up in an endless recursion when checking
for equality in the hashtbl operations of the cache.
---
 src/kernel_services/ast_queries/cil.ml    | 20 ++++++++--------
 tests/misc/array_sizeof.i                 | 10 ++++++++
 tests/misc/oracle/array_sizeof.res.oracle | 29 +++++++++++++++++++++++
 3 files changed, 49 insertions(+), 10 deletions(-)
 create mode 100644 tests/misc/array_sizeof.i
 create mode 100644 tests/misc/oracle/array_sizeof.res.oracle

diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index ed1d2206966..a3fd3727f08 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3957,8 +3957,8 @@ let find_sizeof t f =
     | Error (msg, t') -> raise (SizeOfError(msg, t'))
   with Not_found ->
   try
-    let size = f () in
-    TypSize.add t (Size size) ;
+    let t', size = f () in
+    TypSize.add t' (Size size) ;
     size
   with SizeOfError(t',msg) as e ->
     TypSize.add t (Error (t', msg)) ;
@@ -4378,7 +4378,7 @@ and bitsSizeOf t =
       (SizeOfError
          (Format.sprintf "abstract type '%s'" (compFullName comp), t))
   | TComp ({cfields=Some[]}, _) when acceptEmptyCompinfo() ->
-    find_sizeof t (fun () -> 0)
+    find_sizeof t (fun () -> t,0)
   | TComp ({cfields=Some[]} as comp,_) ->
     find_sizeof t
       (fun () ->
@@ -4405,9 +4405,9 @@ and bitsSizeOf t =
          then
            (* On MSVC if we have just a zero-width bitfields then the length
             * is 32 and is not padded  *)
-           32
+           t, 32
          else
-           addTrailing lastoff.oaFirstFree (8 * bytesAlignOf t))
+           t, addTrailing lastoff.oaFirstFree (8 * bytesAlignOf t))
 
   | TComp (comp, _) -> (* Union *)
     find_sizeof t
@@ -4428,14 +4428,14 @@ and bitsSizeOf t =
          (* Note: we treat None above *)
          let max = List.fold_left fold 0 (Option.get comp.cfields) in
          (* Add trailing by simulating adding an extra field *)
-         addTrailing max (8 * bytesAlignOf t))
+         t, addTrailing max (8 * bytesAlignOf t))
 
-  | TArray(bt, Some len, _) ->
+  | TArray(bt, Some len, attrs) ->
     find_sizeof t
       (fun () ->
          begin
-           match (constFold true len).enode with
-             Const(CInt64(l,_,_)) ->
+           match constFold true len with
+             { enode = Const(CInt64(l,_,_)) } as v->
              let sz = Integer.mul (Integer.of_int (bitsSizeOf bt)) l in
              let sz' =
                match Integer.to_int_opt sz with
@@ -4447,7 +4447,7 @@ and bitsSizeOf t =
                        ^"represented with an OCaml int.", t))
 
              in
-             sz' (*WAS: addTrailing sz' (8 * bytesAlignOf t)*)
+             (TArray(bt, Some v,attrs), sz') (*WAS: addTrailing sz' (8 * bytesAlignOf t)*)
            | _ -> raise (SizeOfError ("Array with non-constant length.", t))
          end)
   | TVoid _ ->
diff --git a/tests/misc/array_sizeof.i b/tests/misc/array_sizeof.i
new file mode 100644
index 00000000000..fa364f4725a
--- /dev/null
+++ b/tests/misc/array_sizeof.i
@@ -0,0 +1,10 @@
+/* run.config
+PLUGIN: @EVA_PLUGINS@
+STDOPT:
+*/
+
+int x;
+void main() {
+  unsigned char buf[sizeof(unsigned char[1]) + sizeof(x)];
+  buf[sizeof(buf)];
+}
diff --git a/tests/misc/oracle/array_sizeof.res.oracle b/tests/misc/oracle/array_sizeof.res.oracle
new file mode 100644
index 00000000000..e580c4e0752
--- /dev/null
+++ b/tests/misc/oracle/array_sizeof.res.oracle
@@ -0,0 +1,29 @@
+[kernel] Parsing array_sizeof.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  x ∈ {0}
+[eva:alarm] array_sizeof.i:9: Warning: 
+  accessing out of bounds index.
+  assert
+  sizeof(unsigned char [sizeof(unsigned char [1]) + sizeof(x)]) <
+  (unsigned int)(sizeof(unsigned char [1]) + sizeof(int));
+[eva] Recording results for main
+[eva] done for function main
+[eva] array_sizeof.i:9: assertion 'Eva,index_bound' got final status invalid.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  NON TERMINATING FUNCTION
+[from] Computing for function main
+[from] Non-terminating function main (no dependencies)
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function main:
+  NON TERMINATING - NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main:
+    tmp
+[inout] Inputs for function main:
+    \nothing
-- 
GitLab