Merge pull request #6076 from TGWDB/inlining-bug-6065

Ensure locations are updated during instrumenting preconditions

regression/goto-cc-goto-analyzer/README.md

@@ -0,0 +1,9 @@
+This subdirectory is for tests where goto-cc is used to produce
+a goto binary that is then passed to goto-analyzer. There is also
+the option to have a custom script to produce the goto binary
+should this require special handling or multiple steps. This
+script is run if the root name of the test file has a script with
+the same filename. For example, if the desc file specifies 
+test.c as the test file then the chain.sh script will check for
+the existence of test.sh and if test.sh exists then it will be used
+to build the goto binary (assumed to be test.gb).

regression/goto-cc-goto-analyzer/chain.sh

@@ -9,12 +9,17 @@ is_windows=$3
 options=${*:4:$#-4}
 name=${*:$#}
 name=${name%.c}
+buildgoto=${name}.sh
 
-if [[ "${is_windows}" == "true" ]]; then
-  "${goto_cc}" "${name}.c"
-  mv "${name}.exe" "${name}.gb"
+if test -f ${buildgoto}; then
+  ./${buildgoto} ${goto_cc} ${is_windows}
 else
-  "${goto_cc}" "${name}.c" -o "${name}.gb"
+  if [[ "${is_windows}" == "true" ]]; then
+    "${goto_cc}" "${name}.c"
+    mv "${name}.exe" "${name}.gb"
+  else
+    "${goto_cc}" "${name}.c" -o "${name}.gb"
+  fi
 fi
 
 "${goto_analyzer}" "${name}.gb" ${options}

regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c

@@ -0,0 +1,54 @@
+// This file is highly reduced from some open source projects.
+// The following four lines are adapted from the openssl library
+// Full repository here:
+// Exact file adapted from here: https://github.com/openssl/openssl/tree/master
+// https://github.com/openssl/openssl/blob/master/crypto/evp/evp_local.h
+struct evp_md_ctx_st
+{
+  const void *digest;
+};
+// The rest of this file is adapted from, various files in the
+// AWS s2n library. Full repository and licence information is
+// available here: https://github.com/aws/s2n-tls
+// Note that this is a highly cut down synthesis of many files
+// with most of their content and structure reduced.
+struct s2n_evp_digest
+{
+  const void *ctx;
+};
+union s2n_hash_low_level_digest {
+};
+struct s2n_hash_evp_digest
+{
+  struct s2n_evp_digest evp_md5_secondary;
+};
+struct s2n_hash_state
+{
+  const struct s2n_hash *hash_impl;
+  union {
+    union s2n_hash_low_level_digest low_level;
+    struct s2n_hash_evp_digest high_level;
+  } digest;
+};
+struct s2n_hash
+{
+  int (*free)(struct s2n_hash_state *state);
+};
+void EVP_MD_CTX_free(struct evp_md_ctx_st *ctx)
+{
+  free(ctx->digest);
+  free(ctx);
+}
+static int s2n_evp_hash_free(struct s2n_hash_state *state)
+{
+  (EVP_MD_CTX_free((state->digest.high_level.evp_md5_secondary.ctx)));
+  return 0;
+}
+static const struct s2n_hash s2n_evp_hash = {
+  .free = &s2n_evp_hash_free,
+};
+static int s2n_hash_set_impl(struct s2n_hash_state *state)
+{
+  state->hash_impl = &s2n_evp_hash;
+  return 0;
+}

regression/goto-cc-goto-analyzer/instrument_preconditions_locations/simple.c

@@ -0,0 +1,5 @@
+// This is highly adapted from the AWS s2n library.
+// Full repository and information here: https://github.com/aws/s2n-tls
+void s2n_hash_free_harness()
+{
+}

regression/goto-cc-goto-analyzer/instrument_preconditions_locations/test.desc

@@ -0,0 +1,16 @@
+CORE
+test.c
+--verify
+^EXIT=0$
+^SIGNAL=0$
+Checking assertions
+^\[EVP_MD_CTX_free.precondition_instance.1\] line \d+ free argument must be NULL or valid pointer: SUCCESS
+--
+Invariant check failed
+--
+This test checks that after building the goto binary (see test.sh)
+that there is no errors that lead to invariant violations.
+This was created after a bug was found due to the
+instrument_preconditions code not correctly fixing locations and
+the invariant check of partial inlining detecting this location
+inconsistency.

regression/goto-cc-goto-analyzer/instrument_preconditions_locations/test.sh

@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+set -e
+
+goto_cc=$1
+is_windows=$2
+
+if [[ "${is_windows}" == "true" ]]; then
+  ${goto_cc}  --export-file-local-symbols  simple.c 
+  mv simple.exe simple.gb
+  ${goto_cc}  --export-file-local-symbols  s2n_hash_inlined.c
+  mv s2n_hash_inlined.exe s2n_hash_inlined.gb
+  ${goto_cc}  --function s2n_hash_free_harness simple.gb s2n_hash_inlined.gb
+  mv simple.exe test.gb
+else
+  ${goto_cc}  --export-file-local-symbols  simple.c -o simple.gb
+  ${goto_cc}  --export-file-local-symbols  s2n_hash_inlined.c -o s2n_hash_inlined.gb
+  ${goto_cc}  --function s2n_hash_free_harness simple.gb s2n_hash_inlined.gb -o test.gb
+fi

src/goto-programs/instrument_preconditions.cpp

@@ -141,6 +141,12 @@ void instrument_preconditions(goto_modelt &goto_model)
   // now remove the preconditions
   for(auto &f_it : goto_model.goto_functions.function_map)
     remove_preconditions(f_it.second.body);
+  // The above may leave some locations uninitialized, this update is a
+  // sanity to check to ensure the goto model and functions are correct
+  // for later passes.
+  // Note that only the first loop is the one known to leave locations
+  // uninitialized.
+  goto_model.goto_functions.update();
 }
 
 void remove_preconditions(goto_functiont &goto_function)