From cdd812a7c0637826251f46f4f24172afb636243a Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 14 Oct 2020 16:12:57 +0100 Subject: [PATCH] 6xxx strlen and 9xxx conclusions. --- 2020-frama-c/6000-strverscmp.html | 78 ++++++++++++++++++++++++++++++++++++ 2020-frama-c/6100-strlen-1.html | 20 +++++++++ 2020-frama-c/6200-strlen-2.html | 51 +++++++++++++++++++++++ 2020-frama-c/6300-strlen.html | 17 ++++++++ 2020-frama-c/6400-strlen.html | 33 +++++++++++++++ 2020-frama-c/6500-strlen.term | 14 +++++++ 2020-frama-c/9000-conclusions-1.html | 17 ++++++++ 2020-frama-c/9100-conclusions-2.html | 17 ++++++++ 2020-frama-c/9200-alternatives.html | 17 ++++++++ 2020-frama-c/9300-resources.html | 30 ++++++++++++++ 10 files changed, 294 insertions(+) create mode 100644 2020-frama-c/6000-strverscmp.html create mode 100644 2020-frama-c/6100-strlen-1.html create mode 100644 2020-frama-c/6200-strlen-2.html create mode 100644 2020-frama-c/6300-strlen.html create mode 100644 2020-frama-c/6400-strlen.html create mode 100755 2020-frama-c/6500-strlen.term create mode 100644 2020-frama-c/9000-conclusions-1.html create mode 100644 2020-frama-c/9100-conclusions-2.html create mode 100644 2020-frama-c/9200-alternatives.html create mode 100644 2020-frama-c/9300-resources.html diff --git a/2020-frama-c/6000-strverscmp.html b/2020-frama-c/6000-strverscmp.html new file mode 100644 index 0000000..132ae68 --- /dev/null +++ b/2020-frama-c/6000-strverscmp.html @@ -0,0 +1,78 @@ + + + + +

glibc strverscmp

+ +
+/* Compare S1 and S2 as strings holding indices/version numbers,
+   returning less than, equal to or greater than zero if S1 is less than,
+   equal to or greater than S2 (for more info, see the texinfo doc).
+*/
+
+int
+__strverscmp (const char *s1, const char *s2)
+{
+  const unsigned char *p1 = (const unsigned char *) s1;
+  const unsigned char *p2 = (const unsigned char *) s2;
+
+  /* Symbol(s)    0       [1-9]   others
+     Transition   (10) 0  (01) d  (00) x   */
+  static const uint8_t next_state[] =
+  {
+      /* state    x    d    0  */
+      /* S_N */  S_N, S_I, S_Z,
+      /* S_I */  S_N, S_I, S_I,
+      /* S_F */  S_N, S_F, S_F,
+      /* S_Z */  S_N, S_F, S_Z
+  };
+
+  static const int8_t result_type[] =
+  {
+      /* state   x/x  x/d  x/0  d/x  d/d  d/0  0/x  0/d  0/0  */
+
+      /* S_N */  CMP, CMP, CMP, CMP, LEN, CMP, CMP, CMP, CMP,
+      /* S_I */  CMP, -1,  -1,  +1,  LEN, LEN, +1,  LEN, LEN,
+      /* S_F */  CMP, CMP, CMP, CMP, CMP, CMP, CMP, CMP, CMP,
+      /* S_Z */  CMP, +1,  +1,  -1,  CMP, CMP, -1,  CMP, CMP
+  };
+
+  if (p1 == p2)
+    return 0;
+
+  unsigned char c1 = *p1++;
+  unsigned char c2 = *p2++;
+  /* Hint: '0' is a digit too.  */
+  int state = S_N + ((c1 == '0') + (__my_isdigit (c1) != 0));
+
+  int diff;
+  while ((diff = c1 - c2) == 0)
+    {
+      if (c1 == '\0')
+	return diff;
+
+      state = next_state[state];
+      c1 = *p1++;
+      c2 = *p2++;
+      state += (c1 == '0') + (__my_isdigit (c1) != 0);
+    }
+
+  state = result_type[state * 3 + (((c2 == '0') + (__my_isdigit (c2) != 0)))];
+
+  switch (state)
+  {
+    case CMP:
+      return diff;
+
+    case LEN:
+      while (__my_isdigit (*p1++))
+	if (!__my_isdigit (*p2++))
+	  return 1;
+
+      return __my_isdigit (*p2) ? -1 : diff;
+
+    default:
+      return state;
+  }
+}
+
diff --git a/2020-frama-c/6100-strlen-1.html b/2020-frama-c/6100-strlen-1.html new file mode 100644 index 0000000..c1e5d08 --- /dev/null +++ b/2020-frama-c/6100-strlen-1.html @@ -0,0 +1,20 @@ + + + + +

glibc strlen (part 1)

+ +
+size_t
+test_strlen (const char *str)
+{
+  const char *char_ptr;
+
+  /* Handle the first few characters by reading one character at a time.
+     Do this until CHAR_PTR is aligned on a longword boundary.  */
+  for (char_ptr = str; ((unsigned long int) char_ptr
+			& (sizeof (longword) - 1)) != 0;
+       ++char_ptr)
+    if (*char_ptr == '\0')
+      return char_ptr - str;
+
diff --git a/2020-frama-c/6200-strlen-2.html b/2020-frama-c/6200-strlen-2.html new file mode 100644 index 0000000..5e27410 --- /dev/null +++ b/2020-frama-c/6200-strlen-2.html @@ -0,0 +1,51 @@ + + + + +

glibc strlen (part 2)

+ +
+  const unsigned long int *longword_ptr;
+  unsigned long int longword, himagic, lomagic;
+
+  longword_ptr = (unsigned long int *) char_ptr;
+
+  himagic = 0x80808080L;
+  lomagic = 0x01010101L;
+  himagic = ((himagic << 16) << 16) | himagic;
+  lomagic = ((lomagic << 16) << 16) | lomagic;
+
+  for (;;)
+    {
+      longword = *longword_ptr++;
+
+      if (((longword - lomagic) & ~longword & himagic) != 0)
+	{
+	  /* Which of the bytes was the zero?  If none of them were, it was
+	     a misfire; continue the search.  */
+
+	  const char *cp = (const char *) (longword_ptr - 1);
+
+	  if (cp[0] == 0)
+	    return cp - str;
+	  if (cp[1] == 0)
+	    return cp - str + 1;
+	  if (cp[2] == 0)
+	    return cp - str + 2;
+	  if (cp[3] == 0)
+	    return cp - str + 3;
+	  if (sizeof (longword) > 4)
+	    {
+	      if (cp[4] == 0)
+		return cp - str + 4;
+	      if (cp[5] == 0)
+		return cp - str + 5;
+	      if (cp[6] == 0)
+		return cp - str + 6;
+	      if (cp[7] == 0)
+		return cp - str + 7;
+	    }
+	}
+    }
+}
+
diff --git a/2020-frama-c/6300-strlen.html b/2020-frama-c/6300-strlen.html new file mode 100644 index 0000000..73e8964 --- /dev/null +++ b/2020-frama-c/6300-strlen.html @@ -0,0 +1,17 @@ + + + + +

glibc strlen specification

+ +
+  /*@
+    requires valid_read_string (str);
+    assigns \nothing;
+    ensures (\forall integer i; 0 <= i < \result ==> str[i] != '\0') &&
+            str[\result] == '\0';
+   */
+  size_t strlen (const char *str)
+  {
+    ...
+
diff --git a/2020-frama-c/6400-strlen.html b/2020-frama-c/6400-strlen.html new file mode 100644 index 0000000..962f06b --- /dev/null +++ b/2020-frama-c/6400-strlen.html @@ -0,0 +1,33 @@ + + + + +

strlen proven, but not by me

+ +
+size_t strlen(const char *s)
+{
+	const char *sc;
+	/*@ loop invariant s <= sc <= s + strlen(s);
+	    loop invariant valid_str(sc);
+	    loop invariant strlen(s) == strlen(sc) + (sc - s);
+	    loop assigns sc;
+	    loop variant strlen(s) - (sc - s);
+	 */
+	for (sc = s; *sc != '\0'; ++sc)
+		/* nothing */;
+	return sc - s;
+}
+
+ +

+Where is the /*@ comment for this function? +We’ll come to that in a minute ... +

+ + +

+Proof by Denis Efremov, Ivannikov Institute for System Programming +at the Russian Academy of Sciences, +https://github.com/evdenis/verker/blob/master/src/strlen.c +

diff --git a/2020-frama-c/6500-strlen.term b/2020-frama-c/6500-strlen.term new file mode 100755 index 0000000..4cdf906 --- /dev/null +++ b/2020-frama-c/6500-strlen.term @@ -0,0 +1,14 @@ +#!/bin/bash - + +source functions + +# Title. +export title="last_char()" + +# History. +remember 'cat snippets/last_char.c' +remember 'frama-c -wp -wp-rte snippets/last_char.c' +remember 'less /usr/share/frama-c/libc/string.h' +remember 'less /usr/share/frama-c/libc/__fc_string_axiomatic.h' + +terminal diff --git a/2020-frama-c/9000-conclusions-1.html b/2020-frama-c/9000-conclusions-1.html new file mode 100644 index 0000000..4426eb0 --- /dev/null +++ b/2020-frama-c/9000-conclusions-1.html @@ -0,0 +1,17 @@ + + + + +

In conclusion (part 1)

+ + diff --git a/2020-frama-c/9100-conclusions-2.html b/2020-frama-c/9100-conclusions-2.html new file mode 100644 index 0000000..c5ea0b3 --- /dev/null +++ b/2020-frama-c/9100-conclusions-2.html @@ -0,0 +1,17 @@ + + + + +

In conclusion (part 2)

+ + diff --git a/2020-frama-c/9200-alternatives.html b/2020-frama-c/9200-alternatives.html new file mode 100644 index 0000000..2469692 --- /dev/null +++ b/2020-frama-c/9200-alternatives.html @@ -0,0 +1,17 @@ + + + + +

Alternatives and related programs

+ + diff --git a/2020-frama-c/9300-resources.html b/2020-frama-c/9300-resources.html new file mode 100644 index 0000000..dcbd13e --- /dev/null +++ b/2020-frama-c/9300-resources.html @@ -0,0 +1,30 @@ + + + + +

Resources

+ + -- 1.8.3.1