From cbc9dd3afde7bd3032fece6396909266d703454d Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 18 Nov 2021 12:09:48 +0100
Subject: [PATCH] [Libc] add more interval function C stubs; add test
---
share/libc/__fc_builtin.c | 59 +++++++++--
tests/libc/fc_builtin_c.c | 37 +++++++
tests/libc/oracle/fc_builtin_c.res.oracle | 114 ++++++++++++++++++++++
3 files changed, 200 insertions(+), 10 deletions(-)
create mode 100644 tests/libc/fc_builtin_c.c
create mode 100644 tests/libc/oracle/fc_builtin_c.res.oracle
diff --git a/share/libc/__fc_builtin.c b/share/libc/__fc_builtin.c
index 2654932223c..b7b973543cc 100644
--- a/share/libc/__fc_builtin.c
+++ b/share/libc/__fc_builtin.c
@@ -22,6 +22,7 @@
#include "__fc_builtin.h"
__PUSH_FC_STDLIB
+#include "limits.h"
/* Those builtins implementations could probably be removed entirely for
Value, as the spec is informative enough. There remains a slight difference
@@ -30,6 +31,11 @@ __PUSH_FC_STDLIB
int volatile Frama_C_entropy_source;
+// Additional entropy sources for some interval functions
+unsigned int volatile __fc_unsigned_int_entropy;
+long volatile __fc_long_entropy;
+unsigned long volatile __fc_unsigned_long_entropy;
+
//@ assigns Frama_C_entropy_source \from Frama_C_entropy_source;
void Frama_C_update_entropy(void) {
Frama_C_entropy_source = Frama_C_entropy_source;
@@ -56,10 +62,10 @@ void *Frama_C_nondet_ptr(void *a, void *b)
int Frama_C_interval(int min, int max)
{
- int r,aux;
+ int r, aux;
Frama_C_update_entropy();
aux = Frama_C_entropy_source;
- if ((aux>=min) && (aux <=max))
+ if (aux >= min && aux <= max)
r = aux;
else
r = min;
@@ -68,27 +74,60 @@ int Frama_C_interval(int min, int max)
char Frama_C_char_interval(char min, char max)
{
- int r;
- char aux;
+ return (char)Frama_C_interval(min, max);
+}
+
+float Frama_C_float_interval(float min, float max)
+{
Frama_C_update_entropy();
- aux = Frama_C_entropy_source;
- if ((aux>=min) && (aux <=max))
+ return Frama_C_entropy_source ? min : max;
+}
+
+double Frama_C_double_interval(double min, double max)
+{
+ Frama_C_update_entropy();
+ return Frama_C_entropy_source ? min : max;
+}
+
+unsigned char Frama_C_unsigned_char_interval(unsigned char min, unsigned char max)
+{
+ return (unsigned char)Frama_C_interval(min, max);
+}
+
+unsigned int Frama_C_unsigned_int_interval(unsigned int min, unsigned int max)
+{
+ unsigned int r, aux;
+ Frama_C_update_entropy();
+ aux = __fc_unsigned_int_entropy;
+ if (aux >= min && aux <= max)
r = aux;
else
r = min;
return r;
}
-float Frama_C_float_interval(float min, float max)
+long Frama_C_long_interval(long min, long max)
{
+ long r, aux;
Frama_C_update_entropy();
- return Frama_C_entropy_source ? min : max;
+ aux = __fc_long_entropy;
+ if (aux >= min && aux <= max)
+ r = aux;
+ else
+ r = min;
+ return r;
}
-double Frama_C_double_interval(double min, double max)
+unsigned long Frama_C_unsigned_long_interval(unsigned long min, unsigned long max)
{
+ unsigned long r, aux;
Frama_C_update_entropy();
- return Frama_C_entropy_source ? min : max;
+ aux = __fc_unsigned_long_entropy;
+ if (aux >= min && aux <= max)
+ r = aux;
+ else
+ r = min;
+ return r;
}
extern void __builtin_abort(void) __attribute__((noreturn)); // GCC builtin
diff --git a/tests/libc/fc_builtin_c.c b/tests/libc/fc_builtin_c.c
new file mode 100644
index 00000000000..ea336b1e04e
--- /dev/null
+++ b/tests/libc/fc_builtin_c.c
@@ -0,0 +1,37 @@
+#include "__fc_builtin.c"
+#include <limits.h>
+
+// The "sampling:unknown" assertions check whether a given value _may_ be
+// in the interval; they are supposed to return 'unknown', but never 'invalid'.
+
+int main() {
+ int i = Frama_C_interval(10, INT_MAX - 20);
+ //@ assert bounds: 10 <= i <= INT_MAX - 20;
+ //@ assert sampling:unknown: i == INT_MAX/2;
+
+ char c = Frama_C_char_interval(CHAR_MIN + 1, CHAR_MAX - 4);
+ //@ assert bounds: CHAR_MIN + 1 <= c <= CHAR_MAX - 4;
+ //@ assert sampling:unknown: c == 42;
+
+ unsigned int ui = Frama_C_unsigned_int_interval(INT_MAX, UINT_MAX);
+ //@ assert bounds: INT_MAX <= ui <= UINT_MAX;
+ //@ assert sampling:unknown: ui == UINT_MAX - 10000;
+
+ float f = Frama_C_float_interval(1.0, 2.0);
+ //@ assert bounds: 1.0 <= f <= 2.0;
+ //@ assert sampling:unknown: f == 1.5;
+
+ double one_e_100 = 0x1.249ad2594c37dp332;
+ double d = Frama_C_double_interval(1e10, one_e_100);
+ //@ assert bounds: 1e10 <= d <= one_e_100;
+ //@ assert sampling:unknown: d == 12345678901.2;
+
+ long l = Frama_C_long_interval(LONG_MIN, -2L);
+ //@ assert bounds: LONG_MIN <= l <= -2;
+ //@ assert sampling:unknown: l == -3;
+
+ unsigned long ul =
+ Frama_C_unsigned_long_interval(LONG_MAX - 1UL, LONG_MAX + 1UL);
+ //@ assert bounds: LONG_MAX - 1 <= ul <= LONG_MAX + 1;
+ //@ assert sampling:unknown: ul == LONG_MAX;
+}
diff --git a/tests/libc/oracle/fc_builtin_c.res.oracle b/tests/libc/oracle/fc_builtin_c.res.oracle
new file mode 100644
index 00000000000..ff75607cc47
--- /dev/null
+++ b/tests/libc/oracle/fc_builtin_c.res.oracle
@@ -0,0 +1,114 @@
+[kernel] Parsing tests/libc/fc_builtin_c.c (with 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
+
+[eva] computing for function Frama_C_interval <- main.
+ Called from tests/libc/fc_builtin_c.c:8.
+[eva] computing for function Frama_C_update_entropy <- Frama_C_interval <- main.
+ Called from share/libc/__fc_builtin.c:66.
+[eva] Recording results for Frama_C_update_entropy
+[eva] Done for function Frama_C_update_entropy
+[eva] Recording results for Frama_C_interval
+[eva] Done for function Frama_C_interval
+[eva] tests/libc/fc_builtin_c.c:9: assertion 'bounds' got status valid.
+[eva:alarm] tests/libc/fc_builtin_c.c:10: Warning:
+ assertion 'sampling,unknown' got status unknown.
+[eva] computing for function Frama_C_char_interval <- main.
+ Called from tests/libc/fc_builtin_c.c:12.
+[eva] computing for function Frama_C_interval <- Frama_C_char_interval <- main.
+ Called from share/libc/__fc_builtin.c:77.
+[eva] share/libc/__fc_builtin.c:66:
+ Reusing old results for call to Frama_C_update_entropy
+[eva] Recording results for Frama_C_interval
+[eva] Done for function Frama_C_interval
+[eva] Recording results for Frama_C_char_interval
+[eva] Done for function Frama_C_char_interval
+[eva] tests/libc/fc_builtin_c.c:13: assertion 'bounds' got status valid.
+[eva:alarm] tests/libc/fc_builtin_c.c:14: Warning:
+ assertion 'sampling,unknown' got status unknown.
+[eva] computing for function Frama_C_unsigned_int_interval <- main.
+ Called from tests/libc/fc_builtin_c.c:16.
+[eva] share/libc/__fc_builtin.c:100:
+ Reusing old results for call to Frama_C_update_entropy
+[eva] Recording results for Frama_C_unsigned_int_interval
+[eva] Done for function Frama_C_unsigned_int_interval
+[eva] tests/libc/fc_builtin_c.c:17: assertion 'bounds' got status valid.
+[eva:alarm] tests/libc/fc_builtin_c.c:18: Warning:
+ assertion 'sampling,unknown' got status unknown.
+[eva] computing for function Frama_C_float_interval <- main.
+ Called from tests/libc/fc_builtin_c.c:20.
+[eva] share/libc/__fc_builtin.c:82:
+ Reusing old results for call to Frama_C_update_entropy
+[eva] Recording results for Frama_C_float_interval
+[eva] Done for function Frama_C_float_interval
+[eva] tests/libc/fc_builtin_c.c:21: assertion 'bounds' got status valid.
+[eva:alarm] tests/libc/fc_builtin_c.c:22: Warning:
+ assertion 'sampling,unknown' got status unknown.
+[eva] computing for function Frama_C_double_interval <- main.
+ Called from tests/libc/fc_builtin_c.c:25.
+[eva] share/libc/__fc_builtin.c:88:
+ Reusing old results for call to Frama_C_update_entropy
+[eva] Recording results for Frama_C_double_interval
+[eva] Done for function Frama_C_double_interval
+[eva] tests/libc/fc_builtin_c.c:26: assertion 'bounds' got status valid.
+[eva:alarm] tests/libc/fc_builtin_c.c:27: Warning:
+ assertion 'sampling,unknown' got status unknown.
+[eva] computing for function Frama_C_long_interval <- main.
+ Called from tests/libc/fc_builtin_c.c:29.
+[eva] share/libc/__fc_builtin.c:112:
+ Reusing old results for call to Frama_C_update_entropy
+[eva] Recording results for Frama_C_long_interval
+[eva] Done for function Frama_C_long_interval
+[eva] tests/libc/fc_builtin_c.c:30: assertion 'bounds' got status valid.
+[eva:alarm] tests/libc/fc_builtin_c.c:31: Warning:
+ assertion 'sampling,unknown' got status unknown.
+[eva] computing for function Frama_C_unsigned_long_interval <- main.
+ Called from tests/libc/fc_builtin_c.c:34.
+[eva] share/libc/__fc_builtin.c:124:
+ Reusing old results for call to Frama_C_update_entropy
+[eva] Recording results for Frama_C_unsigned_long_interval
+[eva] Done for function Frama_C_unsigned_long_interval
+[eva] tests/libc/fc_builtin_c.c:35: assertion 'bounds' got status valid.
+[eva:alarm] tests/libc/fc_builtin_c.c:36: Warning:
+ assertion 'sampling,unknown' got status unknown.
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function Frama_C_update_entropy:
+ Frama_C_entropy_source ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_double_interval:
+ Frama_C_entropy_source ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_float_interval:
+ Frama_C_entropy_source ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_interval:
+ Frama_C_entropy_source ∈ [--..--]
+ r ∈ [-127..2147483627]
+ aux ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_char_interval:
+ Frama_C_entropy_source ∈ [--..--]
+ __retres ∈ [-127..123]
+[eva:final-states] Values at end of function Frama_C_long_interval:
+ Frama_C_entropy_source ∈ [--..--]
+ r ∈ [-2147483648..-2]
+ aux ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_unsigned_int_interval:
+ Frama_C_entropy_source ∈ [--..--]
+ r ∈ [2147483647..4294967295]
+ aux ∈ [--..--]
+[eva:final-states] Values at end of function Frama_C_unsigned_long_interval:
+ Frama_C_entropy_source ∈ [--..--]
+ r ∈ {2147483646; 2147483647; 2147483648}
+ aux ∈ [--..--]
+[eva:final-states] Values at end of function main:
+ Frama_C_entropy_source ∈ [--..--]
+ i ∈ {1073741823}
+ c ∈ {42}
+ ui ∈ {4294957295}
+ f ∈ {1.5}
+ one_e_100 ∈ {1e+100}
+ d ∈ [12345678901.2 .. 12345678901.2]
+ l ∈ {-3}
+ ul ∈ {2147483647}
+ __retres ∈ {0}
--
GitLab