From be74c2e1f841d8b54742adc8c2c2e91e297d76b7 Mon Sep 17 00:00:00 2001
From: Oscar Abrina <abrinao@amazon.com>
Date: Tue, 27 Apr 2021 12:48:00 -0700
Subject: [PATCH] Implement CBMC proof for SigV4_AwsIotDateToIso8601

---
 test/cbmc/proofs/Makefile-project-defines     |  5 +++
 test/cbmc/proofs/Makefile-template-defines    |  4 +-
 .../proofs/SigV4_AwsIotDateToIso8601/Makefile |  2 +-
 .../SigV4_AwsIotDateToIso8601_harness.c       | 42 ++++++++++++++-----
 4 files changed, 39 insertions(+), 14 deletions(-)

diff --git a/test/cbmc/proofs/Makefile-project-defines b/test/cbmc/proofs/Makefile-project-defines
index f6f7681f..56bdd7c3 100644
--- a/test/cbmc/proofs/Makefile-project-defines
+++ b/test/cbmc/proofs/Makefile-project-defines
@@ -15,6 +15,8 @@
 
 # Flags to pass to goto-cc for compilation (typically those passed to gcc -c)
 # COMPILE_FLAGS =
+COMPILE_FLAGS += -fPIC
+COMPILE_FLAGS += -std=gnu90
 
 # Flags to pass to goto-cc for linking (typically those passed to gcc)
 # LINK_FLAGS =
@@ -26,9 +28,12 @@
 # include directories in your project.
 #
 # INCLUDES =
+INCLUDES += -I$(SRCDIR)/test/cbmc/include
+INCLUDES += -I$(SRCDIR)/source/include
 
 # Preprocessor definitions -D...
 # DEFINES =
+DEFINES += -DSIGV4_DO_NOT_USE_CUSTOM_CONFIG=1
 
 # Path to arpa executable
 # ARPA =
diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines
index a292f48d..76cecba0 100644
--- a/test/cbmc/proofs/Makefile-template-defines
+++ b/test/cbmc/proofs/Makefile-template-defines
@@ -1,3 +1,4 @@
+PROOF_ROOT ?= $(abspath .)
 
 # Absolute path to the root of the source tree.
 #
@@ -6,7 +7,7 @@ SRCDIR ?= $(abspath $(PROOF_ROOT)/../../..)
 
 # Absolute path to the litani script.
 #
-LITANI ?= $(abspath $(PROOF_ROOT)/../litani)
+LITANI ?= $(abspath $(PROOF_ROOT)/../litani/litani)
 
 
 # Name of this proof project, displayed in proof reports. For example,
@@ -16,4 +17,3 @@ LITANI ?= $(abspath $(PROOF_ROOT)/../litani)
 # 	  make PROJECT_NAME="FreeRTOS MQTT" report
 #
 PROJECT_NAME = "sigv4-for-aws-iot-embedded-sdk"
-
diff --git a/test/cbmc/proofs/SigV4_AwsIotDateToIso8601/Makefile b/test/cbmc/proofs/SigV4_AwsIotDateToIso8601/Makefile
index c70a9300..75463b72 100644
--- a/test/cbmc/proofs/SigV4_AwsIotDateToIso8601/Makefile
+++ b/test/cbmc/proofs/SigV4_AwsIotDateToIso8601/Makefile
@@ -15,6 +15,6 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/test/cbmc/proofs/source/sigv4.c
+PROJECT_SOURCES += $(SRCDIR)/source/sigv4.c
 
 include ../Makefile.common
diff --git a/test/cbmc/proofs/SigV4_AwsIotDateToIso8601/SigV4_AwsIotDateToIso8601_harness.c b/test/cbmc/proofs/SigV4_AwsIotDateToIso8601/SigV4_AwsIotDateToIso8601_harness.c
index a6045de9..f47ed91e 100644
--- a/test/cbmc/proofs/SigV4_AwsIotDateToIso8601/SigV4_AwsIotDateToIso8601_harness.c
+++ b/test/cbmc/proofs/SigV4_AwsIotDateToIso8601/SigV4_AwsIotDateToIso8601_harness.c
@@ -1,8 +1,23 @@
-// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-// SPDX-License-Identifier: Apache-2.0
-
 /*
- * Insert copyright notice
+ * SigV4 Utility Library v1.0.0
+ * Copyright (C) 2021 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  */
 
 /**
@@ -10,16 +25,21 @@
  * @brief Implements the proof harness for SigV4_AwsIotDateToIso8601 function.
  */
 
-/*
- * Insert project header files that
- *   - include the declaration of the function
- *   - include the types needed to declare function arguments
- */
+/* Include paths for public enums, structures, and macros. */
+#include "sigv4.h"
 
 void harness()
 {
+    char * pInputDate;
+    size_t dateLen;
+    char * pDateISO8601;
+    size_t dateISO8601Len;
+
+    __CPROVER_assume( dateLen < CBMC_MAX_OBJECT_SIZE );
+    pInputDate = malloc( dateLen );
 
-  /* Insert argument declarations */
+    __CPROVER_assume( dateISO8601Len < CBMC_MAX_OBJECT_SIZE );
+    pDateISO8601 = malloc( dateISO8601Len );
 
-  SigV4_AwsIotDateToIso8601( /* Insert arguments */ );
+    SigV4_AwsIotDateToIso8601( pInputDate, dateLen, pDateISO8601, dateISO8601Len );
 }