Replaced --no-externals and --allow-external-sym-calls with --external-calls, updated tests accordingly, and improved documentation on external calls

6 files changed, 25 insertions, 18 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index ddf11929..099123cd 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -103,11 +103,6 @@ namespace {
                    cl::init(true),
 		   cl::desc("Dump test cases for all active states on exit (default=on)"));
   
-  cl::opt<bool>
-  AllowExternalSymCalls("allow-external-sym-calls",
-                        cl::init(false),
-			cl::desc("Allow calls with symbolic arguments to external functions.  This concretizes the symbolic arguments.  (default=off)"));
-
   /// The different query logging solvers that can switched on/off
   enum PrintDebugInstructionsType {
     STDERR_ALL, ///
@@ -185,10 +180,21 @@ namespace {
                 cl::init(false),
                 cl::desc("Generate tests cases for all errors "
                          "(default=off, i.e. one per (error,instruction) pair)"));
-  
-  cl::opt<bool>
-  NoExternals("no-externals", 
-           cl::desc("Do not allow external function calls (default=off)"));
+
+  enum class ExternalCallPolicy {
+    None,     // No external calls allowed
+    Concrete, // Only external calls with concrete arguments allowed
+    All,      // All external calls allowed
+  };
+
+  cl::opt<ExternalCallPolicy>
+  ExternalCalls("external-calls",
+                cl::desc("Specify the external call policy"),
+                cl::values(clEnumValN(ExternalCallPolicy::None, "none", "No external function calls are allowed.  Note that KLEE always allows some external calls with concrete arguments to go through (in particular printf and puts), regardless of this option."),
+                           clEnumValN(ExternalCallPolicy::Concrete, "concrete", "Only external function calls with concrete arguments are allowed (default)"),
+                           clEnumValN(ExternalCallPolicy::All, "all", "All external function calls are allowed.  This concretizes any symbolic arguments in calls to external functions.")
+                           KLEE_LLVM_CL_VAL_END),
+                cl::init(ExternalCallPolicy::Concrete));
 
   cl::opt<bool>
   AlwaysOutputSeeds("always-output-seeds",
@@ -3099,10 +3105,11 @@ void Executor::callExternalFunction(ExecutionState &state,
   if (specialFunctionHandler->handle(state, function, target, arguments))
     return;
   
-  if (NoExternals && !okExternals.count(function->getName())) {
+  if (ExternalCalls == ExternalCallPolicy::None
+      && !okExternals.count(function->getName())) {
     klee_warning("Disallowed call to external function: %s\n",
                function->getName().str().c_str());
-    terminateStateOnError(state, "externals disallowed", User);
+    terminateStateOnError(state, "external calls disallowed", User);
     return;
   }
 
@@ -3115,7 +3122,7 @@ void Executor::callExternalFunction(ExecutionState &state,
   unsigned wordIndex = 2;
   for (std::vector<ref<Expr> >::iterator ai = arguments.begin(), 
        ae = arguments.end(); ai!=ae; ++ai) {
-    if (AllowExternalSymCalls) { // don't bother checking uniqueness
+    if (ExternalCalls == ExternalCallPolicy::All) { // don't bother checking uniqueness
       *ai = optimizer.optimizeExpr(*ai, true);
       ref<ConstantExpr> ce;
       bool success = solver->getValue(state, *ai, ce);
diff --git a/test/CXX/ArrayNew.cpp b/test/CXX/ArrayNew.cpp
index baad95fe..35a4f134 100644
--- a/test/CXX/ArrayNew.cpp
+++ b/test/CXX/ArrayNew.cpp
@@ -1,6 +1,6 @@
 // RUN: %llvmgxx %s -emit-llvm %O0opt -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --no-output --exit-on-error --no-externals %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --no-output --exit-on-error --external-calls=none %t1.bc
 
 #include <cassert>
 
diff --git a/test/CXX/New.cpp b/test/CXX/New.cpp
index 71784f9f..921316a7 100644
--- a/test/CXX/New.cpp
+++ b/test/CXX/New.cpp
@@ -1,6 +1,6 @@
 // RUN: %llvmgxx %s -emit-llvm %O0opt -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --no-output --exit-on-error --no-externals %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --no-output --exit-on-error --external-calls=none %t1.bc
 
 #include <cassert>
 
diff --git a/test/CXX/SimpleVirtual.cpp b/test/CXX/SimpleVirtual.cpp
index 7d0faa08..372b44de 100644
--- a/test/CXX/SimpleVirtual.cpp
+++ b/test/CXX/SimpleVirtual.cpp
@@ -1,6 +1,6 @@
 // RUN: %llvmgxx %s -emit-llvm %O0opt -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --no-output --exit-on-error --no-externals %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --no-output --exit-on-error --external-calls=none %t1.bc
 
 #include <cassert>
 
diff --git a/test/Feature/LowerSwitch.c b/test/Feature/LowerSwitch.c
index 1b280e72..faa82365 100644
--- a/test/Feature/LowerSwitch.c
+++ b/test/Feature/LowerSwitch.c
@@ -1,10 +1,10 @@
 // RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --exit-on-error --allow-external-sym-calls --switch-type=internal %t.bc
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error --external-calls=all --switch-type=internal %t.bc
 // RUN: not test -f %t.klee-out/test000010.ktest
 
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --exit-on-error --allow-external-sym-calls --switch-type=simple %t.bc
+// RUN: %klee --output-dir=%t.klee-out --exit-on-error --switch-type=simple %t.bc
 // RUN: test -f %t.klee-out/test000010.ktest
 
 #include <stdio.h>
diff --git a/test/Runtime/POSIX/MixedConcreteSymbolic.c b/test/Runtime/POSIX/MixedConcreteSymbolic.c
index c32a8f54..71abb116 100644
--- a/test/Runtime/POSIX/MixedConcreteSymbolic.c
+++ b/test/Runtime/POSIX/MixedConcreteSymbolic.c
@@ -1,6 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out -allow-external-sym-calls --exit-on-error --libc=uclibc --posix-runtime %t.bc --sym-stdin 10  2>%t.log | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --external-calls=all --exit-on-error --libc=uclibc --posix-runtime %t.bc --sym-stdin 10  2>%t.log | FileCheck %s
 
 #include "klee/klee.h"
 #include <assert.h>