Improv fromcav (#76)

* Makefile for C bugs

* header prettification

* syntax improvements for Gillian-C logic & preds

* stylings

* bugs in JS in Makefile

* sorting Makefiles

* more

* adding base.c for bugs

* EncryptionHeaderLogic for the bug

* concretisation

* dedicated reductions

* split Makefile for Amazon examples, put them in their respective directories

* add appropriate readmes in the amazon folders

Co-authored-by: pmaksimo <p.maksimovic@imperial.ac.uk>

.vscode/settings.json

@@ -11,8 +11,11 @@
     "__string": "cpp",
     "cstring": "cpp",
     "tuple": "c",
-    "string.h": "c"
-  },
+    "string.h": "c",
+    "random": "c",
+    "ranges": "c",
+    "base.h": "c"
+},
   "python.pythonPath": "/usr/bin/python3",
   "ocaml.sandbox": {
     "kind": "esy",

Gillian-C/examples/amazon/Makefile

@@ -0,0 +1,40 @@
+default:
+	esy x gillian-c verify \
+		header.c edk.c array_list.c ec.c byte_buf.c \
+		hash_table.c string.c allocator.c \
+		error.c base.c \
+		--fstruct-passing --no-lemma-proof -l disabled
+
+proc:
+	esy x gillian-c verify \
+		header.c edk.c array_list.c ec.c byte_buf.c \
+		hash_table.c string.c allocator.c \
+		error.c base.c \
+		--fstruct-passing --no-lemma-proof --proc $(PROC) -l disabled
+
+lemma:
+	esy x gillian-c verify \
+		header.c edk.c array_list.c ec.c byte_buf.c \
+		hash_table.c string.c allocator.c \
+		error.c base.c \
+		--fstruct-passing --no-lemma-proof --lemma $(LEMMA) -l disabled
+
+string-bug:
+	-esy x gillian-c verify \
+		error.c bugs/string.c allocator.c base.c \
+		--no-lemma-proof --proc aws_string_new_from_array -l disabled
+
+header-bug:
+	-esy x gillian-c verify \
+		bugs/header.c edk.c array_list.c ec.c \
+		byte_buf.c hash_table.c string.c allocator.c error.c \
+		bugs/base.c \
+		--fstruct-passing --no-lemma-proof --proc aws_cryptosdk_hdr_parse -l disabled
+
+byte-cursor-ub:
+	-esy x gillian-c verify \
+		bugs/byte_buf.c allocator.c \
+		error.c base.c \
+		--fstruct-passing --no-lemma-proof --proc aws_byte_cursor_advance -l disabled
+
+bugs: string-bug header-bug byte-cursor-ub

Gillian-C/examples/amazon/allocator.c

@@ -4,6 +4,7 @@
  */
 
 #include "allocator.h"
+#include "error.h"
 
 /*@ pred default_allocator(allocator) {
   (allocator -> struct aws_allocator {
@@ -32,12 +33,11 @@ void *s_default_calloc(struct aws_allocator *allocator, size_t num,
     return calloc(num, size);
 }
 
-/* This function is the only one we don't change from the original
- * implementation */
+/* This function is the only one unchanged from the original implementation */
 void *s_default_realloc(struct aws_allocator *allocator, void *ptr,
                         size_t oldsize, size_t newsize) {
-    (void)allocator;
-    (void)oldsize;
+    (void) allocator;
+    (void) oldsize;
 
     if (newsize == 0) {
         free(ptr);
@@ -54,14 +54,6 @@ void *s_default_realloc(struct aws_allocator *allocator, void *ptr,
     return new_mem;
 }
 
-/* The following spec passes */
-/*
-spec aws_mem_acquire (allocator, size) {
-  requires: (allocator == #allocator) * (size == long(#size)) *
-            default_allocator(#allocator) * (0 <# #size)
-  ensures:  UNDEFS(ret, #size)
-}
-*/
 void *aws_mem_acquire(struct aws_allocator *allocator, size_t size) {
     // AWS_FATAL_PRECONDITION(allocator != NULL);
     // AWS_FATAL_PRECONDITION(allocator->mem_acquire != NULL);
@@ -71,17 +63,13 @@ void *aws_mem_acquire(struct aws_allocator *allocator, size_t size) {
     // AWS_FATAL_PRECONDITION(size != 0);
 
     void *mem = allocator->mem_acquire(allocator, size);
-    // Gillian's allocation always works
-    // if (!mem) {
-    //     aws_raise_error(AWS_ERROR_OOM);
-    // }
+    if (!mem) {
+         aws_raise_error(AWS_ERROR_OOM);
+    }
     return mem;
 }
 
 void aws_mem_release(struct aws_allocator *allocator, void *ptr) {
-    // AWS_FATAL_PRECONDITION(allocator != NULL);
-    // AWS_FATAL_PRECONDITION(allocator->mem_release != NULL);
-
     if (ptr != NULL) {
         allocator->mem_release(allocator, ptr);
     }

Gillian-C/examples/amazon/array_list.c

@@ -1,106 +1,108 @@
 #include "array_list.h"
 #include "edk.h"
 #include "error.h"
+
 /*  One can look at the following validity check to understand
     the following predicates :
     https://github.com/awslabs/aws-c-common/blob/bb797381f3468e6f076e53eddbb399a99f54f67b/include/aws/common/array_list.inl#L82
 
     The size of an edk is 96
 */
-/* Unfortunately, we can't go fully polymorphic here, because we don't have a
-   core predicate for arbitrary structs. It has to do with the lack of
-   structures in Csharpminor, but writing a compiler straight from C would let
-   us do that better.
+/*
+    Unfortunately, we cannot go fully polymorphic here, because we don't have a
+    core predicate for arbitrary structs. It has to do with the lack of
+    structures in Csharpminor, but writing a compiler straight from C would let
+    us do that better.
 */
+// Various predicates for dealing with array lists of edks
 /*@
 
-pred edk_array_list_content_pref(+data, +size, +alloc, content) {
-    (size == 0) * (content == []);
-    (0 <=# (size - 96)) *
-    valid_aws_cryptosdk_edk_ptr(data, alloc, #edk) *
-    (content == #edk :: #rest) *
-    (#next == data p+ 96) *
-    edk_array_list_content_pref(#next, size - 96, alloc, #rest)
-}
+    pred edk_array_list_content_pref(+data, +size, +alloc, content) {
+        (size == 0) * (content == []);
+        (0 <=# (size - 96)) *
+        valid_aws_cryptosdk_edk_ptr(data, alloc, #edk) *
+        (content == #edk :: #rest) *
+        (#next == data p+ 96) *
+        edk_array_list_content_pref(#next, size - 96, alloc, #rest)
+    }
 
-lemma array_list_content_pref_is_array(data, size, alloc) {
-    hypothesis: edk_array_list_content_pref(#data, #size, #alloc, #content) * (0 <# #size)
-    conclusions: ARRAY(#data, char, #size, #something)
-    proof: unfold edk_array_list_content_pref(#data, #size, #alloc, #content);
-           if (0 < (#size - 96)) {
-               apply array_list_content_pref_is_array(#data p+ 96, #size - 96, #alloc);
-               unfold_all i__ptr_add
-           } else {
-               unfold_all edk_array_list_content_pref
-           }
-}
+    lemma array_list_content_pref_is_array(data, size, alloc) {
+        hypothesis:
+            edk_array_list_content_pref(#data, #size, #alloc, #content) * (0 <# #size)
+
+        conclusions:
+            ARRAY(#data, char, #size, #something)
+
+        proof:
+            unfold edk_array_list_content_pref(#data, #size, #alloc, #content);
+            if (0 < (#size - 96)) {
+                apply array_list_content_pref_is_array(#data p+ 96, #size - 96, #alloc);
+                unfold_all i__ptr_add
+            } else {
+                unfold_all edk_array_list_content_pref
+            }
+    }
 
-pred nounfold optPadding(+p, +sz) {
-    (sz == 0);
+    pred nounfold optPadding(+p, +sz) {
+        (sz == 0);
+        (1 <=# sz) * ARRAY(p, char, sz, #fill)
+    }
 
-    (1 <=# sz) * ARRAY(p, char, sz, #fill)
- }
+    pred edk_array_list_data_content(+data, +prefix_size, +total_size, +alloc, content) {
+        (0 <# prefix_size) * (0 <# total_size) * MALLOCED(data, total_size) *
+        edk_array_list_content_pref(data, prefix_size, alloc, content) *
+        (prefix_size == (96 * (len content))) *
+        optPadding(data p+ prefix_size, #rest_size) *
+        (#rest_size == (total_size - prefix_size));
 
-pred edk_array_list_data_content(+data, +prefix_size,
-                                 +total_size, +alloc, content) {
-    (0 <# prefix_size) * (0 <# total_size) * MALLOCED(data, total_size) *
-    edk_array_list_content_pref(data, prefix_size, alloc, content) *
-    (prefix_size == (96 * (len content))) *
-    optPadding(data p+ prefix_size, #rest_size) *
-    (#rest_size == (total_size - prefix_size));
+        (0 == prefix_size) * (0 <# total_size) * MALLOCED(data, total_size) *
+        optPadding(data, total_size) * (content == [])
+    }
 
+    lemma edk_array_list_data_is_freeable(data, prefix_size, total_size, alloc) {
+        hypothesis:
+            edk_array_list_data_content(#data, #prefix_size, #total_size, #alloc, #content)
 
-    (0 == prefix_size) * (0 <# total_size) * MALLOCED(data, total_size) *
-    optPadding(data, total_size) * (content == [])
-}
+        conclusions:
+            MARRAY(#data, char, #total_size, #whatever)
 
-lemma edk_array_list_data_is_freeable(data, prefix_size, total_size, alloc) {
-    hypothesis: edk_array_list_data_content(#data, #prefix_size, #total_size, #alloc, #content)
-    conclusions: MARRAY(#data, char, #total_size, #whatever)
-    proof: unfold edk_array_list_data_content(#data, #prefix_size, #total_size, #alloc, #content);
-           if (0 < #prefix_size) {
-            apply array_list_content_pref_is_array(#data, #prefix_size, #alloc)
-           };
-           unfold optPadding(#data p+ #prefix_size, #total_size - #prefix_size)
-}
+        proof:
+            unfold edk_array_list_data_content(#data, #prefix_size, #total_size, #alloc, #content);
+            if (0 < #prefix_size) {
+                apply array_list_content_pref_is_array(#data, #prefix_size, #alloc)
+            };
+            unfold optPadding(#data p+ #prefix_size, #total_size - #prefix_size)
+    }
 
-pred nounfold valid_edk_array_list(+current_size, +length,
-                          +item_size, +data, +alloc, content) {
-  (current_size == 0) * (length == 0) * (item_size == 96) *
-  (data == NULL) * (content == []);
-
-  (item_size == 96) * (0 <=# length) * (0 <# current_size) *
-  aws_mul_u64_checked(item_size, length, #required_size) *
-  (#required_size <=# current_size) *
-  (not (data == NULL)) *
-  edk_array_list_data_content(data, #required_size,
-                              current_size, alloc, content) *
-  (length == len content)
-}
+    pred nounfold valid_edk_array_list(+current_size, +length, +item_size, +data, +alloc, content) {
+        (current_size == 0) * (length == 0) * (item_size == 96) *
+        (data == NULL) * (content == []);
 
-pred valid_edk_array_list_fields(+fields, alloc, content) {
-  (fields == [ alloc, long(#current_size), long(#length),
-               long(#item_size), #data ]) *
-  valid_edk_array_list(#current_size, #length,
-                       #item_size, #data, alloc, content)
-}
+        (item_size == 96) * (0 <=# length) * (0 <# current_size) *
+        aws_mul_u64_checked(item_size, length, #required_size) *
+        (#required_size <=# current_size) *
+        (not (data == NULL)) *
+        edk_array_list_data_content(data, #required_size, current_size, alloc, content) *
+        (length == len content)
+    }
 
-pred empty_edk_array_list_fields(+fields, alloc) {
-    valid_edk_array_list_fields(fields, alloc, [])
-}
+    pred valid_edk_array_list_fields(+fields, alloc, content) {
+        (fields == [ alloc, long(#current_size), long(#length), long(#item_size), #data ]) *
+        valid_edk_array_list(#current_size, #length, #item_size, #data, alloc, content)
+    }
 
-pred nounfold valid_edk_array_list_ptr(+list, alloc, content) {
-  (list -> struct aws_array_list {
-      alloc; long(#current_size); long(#length); long(#item_size); #data
-  }) *
-  valid_edk_array_list(#current_size, #length,
-                       #item_size, #data, alloc, content)
-}
+    pred empty_edk_array_list_fields(+fields, alloc) {
+        valid_edk_array_list_fields(fields, alloc, [])
+    }
 
-pred empty_edk_array_list_ptr(+list, alloc) {
-  valid_edk_array_list_ptr(list, alloc, [])
-}
+    pred nounfold valid_edk_array_list_ptr(+list, alloc, content) {
+        (list -> struct aws_array_list { alloc; long(#current_size); long(#length); long(#item_size); #data}) *
+        valid_edk_array_list(#current_size, #length, #item_size, #data, alloc, content)
+    }
 
+    pred empty_edk_array_list_ptr(+list, alloc) {
+        valid_edk_array_list_ptr(list, alloc, [])
+    }
 */
 
 /*
@@ -284,10 +286,6 @@ int aws_array_list_set_at(struct aws_array_list *list, const void *val,
     memcpy((void *)((uint8_t *)list->data + (list->item_size * index)), val,
            list->item_size);
 
-    /*
-     * This isn't perfect, but its the best I can come up with for detecting
-     * length changes.
-     */
     if (index >= aws_array_list_length(list)) {
         if (aws_add_size_checked(index, 1, &list->length)) {
             // AWS_POSTCONDITION(aws_array_list_is_valid(list));