Merge pull request #1171 from MartinSpiessl/uthash

Add tasks based on the uthash hashing library

Author: dbeyer

c/SoftwareSystems-uthash-MemSafety.set

@@ -0,0 +1,2 @@
+# Contains problems from the software system BusyBox.
+uthash-2.0.2/*.yml

c/SoftwareSystems-uthash-NoOverflows.set

@@ -0,0 +1,2 @@
+# Contains problems from the software system BusyBox.
+uthash-2.0.2/*.yml

c/SoftwareSystems-uthash-ReachSafety.set

@@ -0,0 +1,2 @@
+# Contains problems from the software system BusyBox.
+uthash-2.0.2/*.yml

c/Termination-Other.set

@@ -34,3 +34,4 @@ memsafety-ext/*.yml
 ldv-memsafety/*.yml
 ldv-memsafety-bitfields/*.yml
 pthread-atomic/*.yml
+uthash-2.0.2/*.yml

c/uthash-2.0.2/LICENSE.txt

@@ -0,0 +1,21 @@
+Copyright (c) 2005-2018, Troy D. Hanson    http://troydhanson.github.com/uthash/
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+

c/uthash-2.0.2/Makefile

@@ -0,0 +1,3 @@
+LEVEL := ../
+
+include $(LEVEL)/Makefile.config

c/uthash-2.0.2/README.txt

@@ -0,0 +1,32 @@
+Tasks in this directory were instrumented and added by Martin Spiessl.
+
+These tasks are test cases for the uthash hashing library,
+which is implemented as a preprocessor macro.
+
+As such they are currently purely deterministic, but I think they will still pose a challenge
+to verifiers because of their complexity and extensive heap memory handling.
+
+Currently I only took the first 10 test cases with 6 of the 7 possible hash function.
+The last hash function murmur hash exploits no-strict-aliasing,
+which is undefined behavior and was therefore excluded.
+The tests as they were did not cleanup memory properly.
+I also added a fixed version of the tasks. For some however,
+this fix is insufficient and leads to memory leaks,
+in which case a third version of the task is also added.
+For test10-3 this is still not enough, so there valid-memtrack
+is still violated, I adapted the verdict accordingly.
+
+This makes a total of currently 138 verification tasks.
+
+The .c files were preprocessed with gcc -E -P -m32 $filename
+
+I refrained from formatting the preprocessed files e.g. via clang-formatter because 
+verifiers should be able to cope with file that have multiple statements in one line.
+
+Have fun with solving these tasks!
+
+The license of uthash is essentially the 1-clause BSD license,
+I just copied the LICENSE file from the uthash repository over.
+I put the instrumentation code I added to create these tasks
+under the same license for convenience.
+The version of uthash in these benchmarks is (the tag) 2.0.2

c/uthash-2.0.2/uthash_BER.h

@@ -0,0 +1,78 @@
+#include "uthash_BER.h"
+#include <stdlib.h>   /* malloc */
+#include <assert.h>
+// BEGIN HARNESS
+void reach_error() {
+  assert(0);
+}
+
+void __VERIFIER_assert(int cond) {
+  if (!cond) {
+    reach_error();
+  }
+}
+int count_int_int = 0;
+
+void test_int_int(int a, int b){
+  switch (count_int_int++) {
+     case 0:
+       __VERIFIER_assert((a == 0) && (b == 0));
+       break;
+     case 1:
+       __VERIFIER_assert((a == 1) && (b == 1));
+       break;
+     case 2:
+       __VERIFIER_assert((a == 2) && (b == 4));
+       break;
+     case 3:
+       __VERIFIER_assert((a == 3) && (b == 9));
+       break;
+     case 4:
+       __VERIFIER_assert((a == 4) && (b == 16));
+       break;
+     case 5:
+       __VERIFIER_assert((a == 5) && (b == 25));
+       break;
+     case 6:
+       __VERIFIER_assert((a == 6) && (b == 36));
+       break;
+     case 7:
+       __VERIFIER_assert((a == 7) && (b == 49));
+       break;
+     case 8:
+       __VERIFIER_assert((a == 8) && (b == 64));
+       break;
+     case 9:
+       __VERIFIER_assert((a == 9) && (b == 81));
+       break;
+  }
+}
+// END HARNESS
+
+typedef struct example_user_t {
+    int id;
+    int cookie;
+    UT_hash_handle hh;
+} example_user_t;
+
+int main()
+{
+    int i;
+    example_user_t *user, *users=NULL;
+
+    /* create elements */
+    for(i=0; i<10; i++) {
+        user = (example_user_t*)malloc(sizeof(example_user_t));
+        if (user == NULL) {
+            exit(-1);
+        }
+        user->id = i;
+        user->cookie = i*i;
+        HASH_ADD_INT(users,id,user);
+    }
+
+    for(user=users; user != NULL; user=(example_user_t*)(user->hh.next)) {
+        test_int_int(user->id, user->cookie);
+    }
+    return 0;
+}