Moved string functions to the .c where they belong (#481)

* Moved string functions to the .c where they belong

* fix CBMC tests by adding string.c

* moved functions back inline as requested in PR

.cbmc-batch/jobs/aws_hash_c_string/Makefile

@@ -33,6 +33,7 @@ DEPENDENCIES += $(HELPERDIR)/source/utils.c
 DEPENDENCIES += $(HELPERDIR)/stubs/error.c
 DEPENDENCIES += $(SRCDIR)/source/common.c
 DEPENDENCIES += $(SRCDIR)/source/hash_table.c
+DEPENDENCIES += $(SRCDIR)/source/string.c
 
 ENTRY = aws_hash_c_string_harness
 ###########

.cbmc-batch/jobs/aws_hash_c_string/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-jobos: ubuntu16
 cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;strlen.0:33,__CPROVER_file_local_lookup3_inl_hashlittle2.0:3,__CPROVER_file_local_lookup3_inl_hashlittle2.1:3,__CPROVER_file_local_lookup3_inl_hashlittle2.2:3;--object-bits;8"
-goto: aws_hash_c_string_harness.goto
 expected: "SUCCESSFUL"
+goto: aws_hash_c_string_harness.goto
+jobos: ubuntu16

.cbmc-batch/jobs/aws_hash_callback_c_str_eq/Makefile

@@ -28,8 +28,10 @@ DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
 DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
 DEPENDENCIES += $(HELPERDIR)/source/utils.c
 DEPENDENCIES += $(HELPERDIR)/stubs/memcmp_override.c
-DEPENDENCIES += $(SRCDIR)/source/hash_table.c
 DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/hash_table.c
+DEPENDENCIES += $(SRCDIR)/source/string.c
+
 
 ENTRY = aws_hash_callback_c_str_eq_harness
 

.cbmc-batch/jobs/aws_hash_callback_c_str_eq/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-jobos: ubuntu16
 cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;strcmp.0:65,strlen.0:65;--object-bits;8"
-goto: aws_hash_callback_c_str_eq_harness.goto
 expected: "SUCCESSFUL"
+goto: aws_hash_callback_c_str_eq_harness.goto
+jobos: ubuntu16

.cbmc-batch/jobs/aws_hash_callback_string_eq/Makefile

@@ -28,8 +28,10 @@ DEPENDENCIES += $(HELPERDIR)/source/make_common_data_structures.c
 DEPENDENCIES += $(HELPERDIR)/source/proof_allocators.c
 DEPENDENCIES += $(HELPERDIR)/source/utils.c
 DEPENDENCIES += $(HELPERDIR)/stubs/memcmp_override.c
-DEPENDENCIES += $(SRCDIR)/source/hash_table.c
 DEPENDENCIES += $(SRCDIR)/source/byte_buf.c
+DEPENDENCIES += $(SRCDIR)/source/hash_table.c
+DEPENDENCIES += $(SRCDIR)/source/string.c
+
 
 ENTRY = aws_hash_callback_string_eq_harness
 

.cbmc-batch/jobs/aws_hash_callback_string_eq/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-jobos: ubuntu16
 cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;memcmp.0:97;--object-bits;8"
-goto: aws_hash_callback_string_eq_harness.goto
 expected: "SUCCESSFUL"
+goto: aws_hash_callback_string_eq_harness.goto
+jobos: ubuntu16

.cbmc-batch/jobs/aws_hash_string/Makefile

@@ -32,6 +32,7 @@ DEPENDENCIES += $(HELPERDIR)/source/utils.c
 DEPENDENCIES += $(HELPERDIR)/stubs/error.c
 DEPENDENCIES += $(SRCDIR)/source/common.c
 DEPENDENCIES += $(SRCDIR)/source/hash_table.c
+DEPENDENCIES += $(SRCDIR)/source/string.c
 
 ENTRY = aws_hash_string_harness
 ###########

.cbmc-batch/jobs/aws_hash_string/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-jobos: ubuntu16
 cbmcflags: "--bounds-check;--div-by-zero-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--unwindset;__CPROVER_file_local_lookup3_inl_hashlittle2.0:3,__CPROVER_file_local_lookup3_inl_hashlittle2.1:3,__CPROVER_file_local_lookup3_inl_hashlittle2.2:3;--object-bits;8"
-goto: aws_hash_string_harness.goto
 expected: "SUCCESSFUL"
+goto: aws_hash_string_harness.goto
+jobos: ubuntu16

include/aws/common/string.h

@@ -57,152 +57,52 @@ struct aws_string {
 #    pragma warning(pop)
 #endif
 
-/**
- * Evaluates the set of properties that define the shape of all valid aws_string structures.
- * It is also a cheap check, in the sense it run in constant time (i.e., no loops or recursion).
- */
-AWS_STATIC_IMPL bool aws_string_is_valid(const struct aws_string *str) {
-    return str && AWS_MEM_IS_READABLE(&str->bytes[0], str->len + 1) && str->bytes[str->len] == 0;
-}
-
-/**
- * Best-effort checks aws_string invariants, when the str->len is unknown
- */
-AWS_STATIC_IMPL bool aws_c_string_is_valid(const char *str) {
-    /* Knowing the actual length to check would require strlen(), which is
-     * a) linear time in the length of the string
-     * b) could already cause a memory violation for a non-zero-terminated string.
-     * But we know that a c-string must have at least one character, to store the null terminator
-     */
-    return str && AWS_MEM_IS_READABLE(str, 1);
-}
-
-/**
- * Equivalent to str->bytes. Here for legacy reasons.
- */
-AWS_STATIC_IMPL const uint8_t *aws_string_bytes(const struct aws_string *str) {
-    AWS_PRECONDITION(aws_string_is_valid(str));
-    return str->bytes;
-}
+AWS_EXTERN_C_BEGIN
 
 /**
  * Returns true if bytes of string are the same, false otherwise.
  */
-AWS_STATIC_IMPL bool aws_string_eq(const struct aws_string *a, const struct aws_string *b) {
-    AWS_PRECONDITION(!a || aws_string_is_valid(a));
-    AWS_PRECONDITION(!b || aws_string_is_valid(b));
-    if (a == b) {
-        return true;
-    }
-    if (a == NULL || b == NULL) {
-        return false;
-    }
-    return aws_array_eq(a->bytes, a->len, b->bytes, b->len);
-}
+AWS_COMMON_API
+bool aws_string_eq(const struct aws_string *a, const struct aws_string *b);
 
 /**
  * Returns true if bytes of string are equivalent, using a case-insensitive comparison.
  */
-AWS_STATIC_IMPL bool aws_string_eq_ignore_case(const struct aws_string *a, const struct aws_string *b) {
-    AWS_PRECONDITION(!a || aws_string_is_valid(a));
-    AWS_PRECONDITION(!b || aws_string_is_valid(b));
-    if (a == b) {
-        return true;
-    }
-    if (a == NULL || b == NULL) {
-        return false;
-    }
-    return aws_array_eq_ignore_case(a->bytes, a->len, b->bytes, b->len);
-}
+AWS_COMMON_API
+bool aws_string_eq_ignore_case(const struct aws_string *a, const struct aws_string *b);
 
 /**
  * Returns true if bytes of string and cursor are the same, false otherwise.
  */
-AWS_STATIC_IMPL bool aws_string_eq_byte_cursor(const struct aws_string *str, const struct aws_byte_cursor *cur) {
-    AWS_PRECONDITION(!str || aws_string_is_valid(str));
-    AWS_PRECONDITION(!cur || aws_byte_cursor_is_valid(cur));
-    if (str == NULL && cur == NULL) {
-        return true;
-    }
-    if (str == NULL || cur == NULL) {
-        return false;
-    }
-    return aws_array_eq(str->bytes, str->len, cur->ptr, cur->len);
-}
+AWS_COMMON_API
+bool aws_string_eq_byte_cursor(const struct aws_string *str, const struct aws_byte_cursor *cur);
 
 /**
  * Returns true if bytes of string and cursor are equivalent, using a case-insensitive comparison.
  */
-AWS_STATIC_IMPL
-bool aws_string_eq_byte_cursor_ignore_case(const struct aws_string *str, const struct aws_byte_cursor *cur) {
-    AWS_PRECONDITION(!str || aws_string_is_valid(str));
-    AWS_PRECONDITION(!cur || aws_byte_cursor_is_valid(cur));
-    if (str == NULL && cur == NULL) {
-        return true;
-    }
-    if (str == NULL || cur == NULL) {
-        return false;
-    }
-    return aws_array_eq_ignore_case(str->bytes, str->len, cur->ptr, cur->len);
-}
+AWS_COMMON_API
+bool aws_string_eq_byte_cursor_ignore_case(const struct aws_string *str, const struct aws_byte_cursor *cur);
 
 /**
  * Returns true if bytes of string and buffer are the same, false otherwise.
  */
-AWS_STATIC_IMPL bool aws_string_eq_byte_buf(const struct aws_string *str, const struct aws_byte_buf *buf) {
-    AWS_PRECONDITION(!str || aws_string_is_valid(str));
-    AWS_PRECONDITION(!buf || aws_byte_buf_is_valid(buf));
-    if (str == NULL && buf == NULL) {
-        return true;
-    }
-    if (str == NULL || buf == NULL) {
-        return false;
-    }
-    return aws_array_eq(str->bytes, str->len, buf->buffer, buf->len);
-}
+AWS_COMMON_API
+bool aws_string_eq_byte_buf(const struct aws_string *str, const struct aws_byte_buf *buf);
 
 /**
  * Returns true if bytes of string and buffer are equivalent, using a case-insensitive comparison.
  */
-AWS_STATIC_IMPL
-bool aws_string_eq_byte_buf_ignore_case(const struct aws_string *str, const struct aws_byte_buf *buf) {
-    AWS_PRECONDITION(!str || aws_string_is_valid(str));
-    AWS_PRECONDITION(!buf || aws_byte_buf_is_valid(buf));
-    if (str == NULL && buf == NULL) {
-        return true;
-    }
-    if (str == NULL || buf == NULL) {
-        return false;
-    }
-    return aws_array_eq_ignore_case(str->bytes, str->len, buf->buffer, buf->len);
-}
+AWS_COMMON_API
+bool aws_string_eq_byte_buf_ignore_case(const struct aws_string *str, const struct aws_byte_buf *buf);
 
-AWS_STATIC_IMPL bool aws_string_eq_c_str(const struct aws_string *str, const char *c_str) {
-    AWS_PRECONDITION(!str || aws_string_is_valid(str));
-    if (str == NULL && c_str == NULL) {
-        return true;
-    }
-    if (str == NULL || c_str == NULL) {
-        return false;
-    }
-    return aws_array_eq_c_str(str->bytes, str->len, c_str);
-}
+AWS_COMMON_API
+bool aws_string_eq_c_str(const struct aws_string *str, const char *c_str);
 
 /**
  * Returns true if bytes of strings are equivalent, using a case-insensitive comparison.
  */
-AWS_STATIC_IMPL bool aws_string_eq_c_str_ignore_case(const struct aws_string *str, const char *c_str) {
-    AWS_PRECONDITION(!str || aws_string_is_valid(str));
-    if (str == NULL && c_str == NULL) {
-        return true;
-    }
-    if (str == NULL || c_str == NULL) {
-        return false;
-    }
-    return aws_array_eq_c_str_ignore_case(str->bytes, str->len, c_str);
-}
-
-AWS_EXTERN_C_BEGIN
+AWS_COMMON_API
+bool aws_string_eq_c_str_ignore_case(const struct aws_string *str, const char *c_str);
 
 /**
  * Constructor functions which copy data from null-terminated C-string or array of bytes.
@@ -252,8 +152,6 @@ int aws_string_compare(const struct aws_string *a, const struct aws_string *b);
 AWS_COMMON_API
 int aws_array_list_comparator_string(const void *a, const void *b);
 
-AWS_EXTERN_C_END
-
 /**
  * Defines a (static const struct aws_string *) with name specified in first
  * argument that points to constant memory and has data bytes containing the
@@ -289,23 +187,38 @@ AWS_EXTERN_C_END
  * accordingly. If there is insufficient space in the buf, returns
  * false, leaving the buf unchanged.
  */
-AWS_STATIC_IMPL bool aws_byte_buf_write_from_whole_string(
+AWS_COMMON_API
+bool aws_byte_buf_write_from_whole_string(
     struct aws_byte_buf *AWS_RESTRICT buf,
-    const struct aws_string *AWS_RESTRICT src) {
-    AWS_PRECONDITION(!buf || aws_byte_buf_is_valid(buf));
-    AWS_PRECONDITION(!src || aws_string_is_valid(src));
-    if (buf == NULL || src == NULL) {
-        return false;
-    }
-    return aws_byte_buf_write(buf, aws_string_bytes(src), src->len);
-}
+    const struct aws_string *AWS_RESTRICT src);
 
 /**
  * Creates an aws_byte_cursor from an existing string.
  */
-AWS_STATIC_IMPL struct aws_byte_cursor aws_byte_cursor_from_string(const struct aws_string *src) {
-    AWS_PRECONDITION(aws_string_is_valid(src));
-    return aws_byte_cursor_from_array(aws_string_bytes(src), src->len);
-}
+AWS_COMMON_API
+struct aws_byte_cursor aws_byte_cursor_from_string(const struct aws_string *src);
+
+AWS_EXTERN_C_END
+
+/**
+ * Equivalent to str->bytes.
+ */
+AWS_STATIC_IMPL
+const uint8_t *aws_string_bytes(const struct aws_string *str);
+
+/**
+ * Evaluates the set of properties that define the shape of all valid aws_string structures.
+ * It is also a cheap check, in the sense it run in constant time (i.e., no loops or recursion).
+ */
+AWS_STATIC_IMPL
+bool aws_string_is_valid(const struct aws_string *str);
+
+/**
+ * Best-effort checks aws_string invariants, when the str->len is unknown
+ */
+AWS_STATIC_IMPL
+bool aws_c_string_is_valid(const char *str);
+
+#include <aws/common/string.inl>
 
 #endif /* AWS_COMMON_STRING_H */

include/aws/common/string.inl

@@ -0,0 +1,49 @@
+#ifndef AWS_COMMON_STRING_INL
+#define AWS_COMMON_STRING_INL
+/*
+ * Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License").
+ * You may not use this file except in compliance with the License.
+ * A copy of the License is located at
+ *
+ *  http://aws.amazon.com/apache2.0
+ *
+ * or in the "license" file accompanying this file. This file is distributed
+ * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
+ * express or implied. See the License for the specific language governing
+ * permissions and limitations under the License.
+ */
+
+/**
+ * Equivalent to str->bytes.
+ */
+AWS_STATIC_IMPL
+const uint8_t *aws_string_bytes(const struct aws_string *str) {
+    AWS_PRECONDITION(aws_string_is_valid(str));
+    return str->bytes;
+}
+
+/**
+ * Evaluates the set of properties that define the shape of all valid aws_string structures.
+ * It is also a cheap check, in the sense it run in constant time (i.e., no loops or recursion).
+ */
+AWS_STATIC_IMPL
+bool aws_string_is_valid(const struct aws_string *str) {
+    return str && AWS_MEM_IS_READABLE(&str->bytes[0], str->len + 1) && str->bytes[str->len] == 0;
+}
+
+/**
+ * Best-effort checks aws_string invariants, when the str->len is unknown
+ */
+AWS_STATIC_IMPL
+bool aws_c_string_is_valid(const char *str) {
+    /* Knowing the actual length to check would require strlen(), which is
+     * a) linear time in the length of the string
+     * b) could already cause a memory violation for a non-zero-terminated string.
+     * But we know that a c-string must have at least one character, to store the null terminator
+     */
+    return str && AWS_MEM_IS_READABLE(str, 1);
+}
+
+#endif /* AWS_COMMON_STRING_INL */