Import ikos 1.1.2

CMakeLists.txt

@@ -41,7 +41,7 @@
 cmake_minimum_required(VERSION 2.8.12.2 FATAL_ERROR)
 
 project(ikos)
-set(PACKAGE_VERSION "1.1.1")
+set(PACKAGE_VERSION "1.1.2")
 
 #
 # Build settings

README.md

@@ -1,4 +1,4 @@
-IKOS v.1.1.1
+IKOS v.1.1.2
 ============
 
 LICENSE

RELEASE_NOTES.md

@@ -1,3 +1,28 @@
+IKOS VERSION 1.1.2 RELEASE NOTES
+================================
+
+RELEASE DATE
+------------
+
+September 2016
+
+LIST OF CHANGES
+---------------
+
+### IKOS Core Changes
+
+* Added interfaces for abstract domains, nullity domains, uninitialized variables domains, pointer domains and memory domains.
+* Moved the pointer domain, the value domain and the summary domain under IKOS core.
+
+### Analyzer Changes
+
+* Added a pass to unify exit nodes.
+
+### ARBOS Changes
+
+* Added APIs to set and retrieve "unreachable" and "unwind" basic blocks in an AR_Code
+
+
 IKOS VERSION 1.1.1 RELEASE NOTES
 ================================
 
@@ -115,27 +140,13 @@ The current implementation of LLVM frontend does not support LLVM vector type (h
 Exception Handling
 ------------------
 
-IKOS 1.1.1 is able to analyze C++ code containing exceptions, but exception propagation through functions is not handled. If the code you are analyzing can raise an exception and does not catch it within the same function, IKOS might be unsound, meaning that it can miss runtime errors. If your code only uses exceptions to report a runtime error and stop the program, then IKOS should be sound.
+IKOS 1.1.2 is able to analyze C++ code containing exceptions, but exception propagation through functions is not handled. If the code you are analyzing can raise an exception and does not catch it within the same function, IKOS might be unsound, meaning that it can miss runtime errors. If your code only uses exceptions to report a runtime error and stop the program, then IKOS should be sound.
 
 Octagon Abstract Domain
 -----------------------
 
 The octagon abstract domain has some implementation issues. Do not use it.
 
-Functions Returning a Temporary Array/Structure
------------------------------------------------
-
-IKOS is unsound if you have a function that returns a temporary array or structure. For instance:
-
-```
-int* f() {
-  int tab[42];
-  return tab;
-}
-```
-
-By the way, this should be forbidden and your compiler should warn you.
-
 Variable Length Array
 ---------------------
 

abs-repr/docs/AR_SPEC.md

@@ -482,10 +482,12 @@ Local variable reference
 ($code
   ($entry ($entry))
   ($exit ($return))
+  ($unreachable ($if.then))
+  ($unwind ($unwind))
   ($basicblocks ($basicblock) ...)
   ($trans ($edge () ()) ...))
 ```
-Note ($exit) may have zero arguments. In this case the function does not terminate with a return block.
+We support three different types of terminating blocks in AR_Code: exit, unreachable, and unwind. In an AR _Code, we allow at most one basic block per type. Using the LLVM frontend, we transform the LLVM IR using the  UnifyFunctionExitNodes pass to acheive this before we translate the LLVM IR to AR. Note that ($exit), ($unreachable), and ($unwind) may have zero arguments, which means these blocks may be absent in the function in the LLVM IR. If the exit block is missing, then this means the function does not terminate with a return block that ends with a return instruction.
 
 #### AR_Basic_Block
 

abs-repr/include/arbos/semantics/ar.hpp

@@ -2549,6 +2549,8 @@ class AR_Code : public AR_Node {
 private:
   index64_t _entry_block;
   index64_t _exit_block;
+  index64_t _unreachable_block;
+  index64_t _unwind_block;
   std::vector< AR_Node_Ref< AR_Basic_Block > > _blocks;
   std::vector< AR_Node_Ref< AR_Internal_Variable > > _internal_variables;
   std::unordered_map< std::string, AR_Node_Ref< AR_Basic_Block > >
@@ -2595,6 +2597,22 @@ class AR_Code : public AR_Node {
     _exit_block = block.getUID();
   }
 
+  inline AR_Node_Ref< AR_Basic_Block > getUnreachableBlock() {
+    return AR_Node_Ref< AR_Basic_Block >(_unreachable_block);
+  }
+
+  inline void setUnreachableBlock(AR_Node_Ref< AR_Basic_Block > block) {
+    _unreachable_block = block.getUID();
+  }
+
+  inline AR_Node_Ref< AR_Basic_Block > getUnwindBlock() {
+    return AR_Node_Ref< AR_Basic_Block >(_unwind_block);
+  }
+
+  inline void setUnwindBlock(AR_Node_Ref< AR_Basic_Block > block) {
+    _unwind_block = block.getUID();
+  }
+
   AR_Node_Ref< AR_Internal_Variable > getInternalVariable(
       const std::string& name);
 
@@ -2622,6 +2640,7 @@ class AR_Code : public AR_Node {
   virtual void accept(std::shared_ptr< Visitor > visitor);
   AR_Node_Ref< AR_Basic_Block > getBasicBlockByNameId(
       const std::string& name_id);
+  index64_t getBasicBlockUIDByName(const std::string& name);
   virtual AR_CLASS_TYPE_CODE getClassType() { return AR_CODE_CLASS_TYPE; }
 
   //! Returns the shared_ptr to AR_Code

abs-repr/src/arbos/api/ar.cpp

@@ -2146,14 +2146,16 @@ AR_Code::AR_Code(index64_t parent_function, s_expression e)
     : AR_Node(),
       _entry_block(0),
       _exit_block(0),
+      _unreachable_block(0),
+      _unwind_block(0),
       _bblocks_connected(false),
       _parent_function(parent_function) {
   /**
    * Example s-expr: ($code ($entry ($init)) ($exit ($init)) ($basicblocks
    * ($basicblock) ...) ($trans ($edge () ()) ...))
    */
-  s_expression_ref en, ex, bbs, t;
-  if (s_pattern("code", s_pattern("entry", en), ex, bbs, t) ^ e) {
+  s_expression_ref en, ex, ur, uw, bbs, t;
+  if (s_pattern("code", s_pattern("entry", en), ex, ur, uw, bbs, t) ^ e) {
     ARModel::Instance()->setCurrentBuildingScope(
         AR_Node_Ref< AR_Code >(getUID()));
 
@@ -2166,17 +2168,21 @@ AR_Code::AR_Code(index64_t parent_function, s_expression e)
     }
     connect_basic_blocks(*t);
 
-    std::string entry_block_name = (static_cast< string_atom& >(**en)).data();
-    _entry_block = (*getBasicBlockByNameId(entry_block_name)).getUID();
-    if ((*ex).n_args() == 0) {
-      _exit_block = 0;
-    } else {
-      std::string exit_block_name =
-          (static_cast< string_atom& >(*(*ex)[1])).data();
-      _exit_block = (exit_block_name.empty())
+    _entry_block =
+        getBasicBlockUIDByName((static_cast< string_atom& >(**en)).data());
+    _exit_block = (*ex).n_args() == 0
+                      ? 0
+                      : getBasicBlockUIDByName(
+                            (static_cast< string_atom& >(*(*ex)[1])).data());
+    _unreachable_block =
+        (*ur).n_args() == 0
+            ? 0
+            : getBasicBlockUIDByName(
+                  (static_cast< string_atom& >(*(*ur)[1])).data());
+    _unwind_block = (*uw).n_args() == 0
                         ? 0
-                        : (*getBasicBlockByNameId(exit_block_name)).getUID();
-    }
+                        : getBasicBlockUIDByName(
+                              (static_cast< string_atom& >(*(*uw)[1])).data());
   } else {
     throw parse_error("AR_Code", e);
   }
@@ -2200,6 +2206,14 @@ void AR_Code::addInternalVariable(
   _internal_variables.push_back(internal_var);
 }
 
+index64_t AR_Code::getBasicBlockUIDByName(const std::string& name) {
+  if (name.empty())
+    return 0;
+  AR_Node_Ref< AR_Basic_Block > bb(_name_to_uid[name]);
+  assert(bb.getUID() > 0);
+  return bb.getUID();
+}
+
 AR_Node_Ref< AR_Basic_Block > AR_Code::getBasicBlockByNameId(
     const std::string& name_id) {
   AR_Node_Ref< AR_Basic_Block > bb(_name_to_uid[name_id]);
@@ -2237,15 +2251,32 @@ AR_Code::~AR_Code() {}
 void AR_Code::print(std::ostream& out) {
   AR_Node_Ref< AR_Basic_Block > entry(_entry_block);
   AR_Node_Ref< AR_Basic_Block > exit(_exit_block);
+  AR_Node_Ref< AR_Basic_Block > unreachable(_unreachable_block);
+  AR_Node_Ref< AR_Basic_Block > unwind(_unwind_block);
 
   out << "entry: " << (*entry).getNameId() << "!" << entry.getUID()
       << std::endl;
+
   if (_exit_block != 0) {
     out << "exit: " << (*exit).getNameId() << "!" << exit.getUID() << std::endl;
   } else {
     out << "exit: none" << std::endl;
   }
 
+  if (_unreachable_block != 0) {
+    out << "unreachable: " << (*unreachable).getNameId() << "!"
+        << unreachable.getUID() << std::endl;
+  } else {
+    out << "unreachable: none" << std::endl;
+  }
+
+  if (_unwind_block != 0) {
+    out << "unwind: " << (*unwind).getNameId() << "!" << unwind.getUID()
+        << std::endl;
+  } else {
+    out << "unwind: none" << std::endl;
+  }
+
   out << std::endl;
   typedef std::vector< AR_Node_Ref< AR_Basic_Block > >::iterator BBIt;
   for (BBIt I = _blocks.begin(), E = _blocks.end(); I != E; ++I) {

abs-repr/tests/regression/tests/parsing/non-term/1/runtest

@@ -2,14 +2,14 @@
 
 source ../../../../utils/test_config.sh
 
-clang -emit-llvm -o test.bc -g -c test.c
-[ -f test.bc ] || { echo >&2 "Test Failed! Cannot generate LLVM bitcode.  Aborting."; exit 1; }
+# test.bc generated using: clang -emit-llvm -o test.bc -g -c test.c
+[ -f test.bc ] || { echo >&2 "Test Failed! LLVM bitcode unavailable.  Aborting."; exit 1; }
 
 opt -load="$LLVM_PASSES_DIR/$llvm_arbos_module" $LLVM_PASSES $PRE_ARBOS_PASSES -arbos -disable-output < test.bc > test.ar
 [ -f test.ar ] || { echo >&2 "Test Failed! Cannot generate AR.  Aborting."; exit 1; }
 
-arbos -load="$ARBOS_PASSES_DIR/$basic_parsing_ar_pass" -hello < test.ar >/dev/null 2>&1 || { echo >&2 "Test Failed! Cannot parse test.ar"; exit 1; }
+arbos -load="$ARBOS_PASSES_DIR/libtest-parsing-exit-nodes.$DYNLIB_EXT" -check-exit-nodes -L main -L return -L if.then -L null < test.ar >/dev/null 2>&1 || { echo >&2 "Test Failed! Cannot parse test.ar"; exit 1; }
 
 echo "Test Passed!"
 
-rm *.bc *.ar
+rm *.ar

abs-repr/tests/regression/verifier-passes/CMakeLists.txt

@@ -10,6 +10,7 @@ add_subdirectory(parsing/call-args)
 add_subdirectory(parsing/check-srcloc)
 add_subdirectory(parsing/gv-init)
 add_subdirectory(parsing/src-lines/1)
+add_subdirectory(parsing/check-exit-nodes)
 add_subdirectory(parsing/basic)
 add_subdirectory(uid/internal_var)
 
@@ -28,4 +29,5 @@ add_custom_target(verifier-passes DEPENDS
   test-parsing-src-lines-1
   test-parsing-uid-internal_var
   test-parsing-basic
+  test-parsing-exit-nodes
 )

abs-repr/tests/regression/verifier-passes/parsing/check-exit-nodes/CMakeLists.txt

@@ -0,0 +1,5 @@
+add_library(test-parsing-exit-nodes SHARED test-parsing-exit-nodes.cpp)
+
+target_link_libraries(test-parsing-exit-nodes arbos-api)
+
+install(TARGETS test-parsing-exit-nodes DESTINATION lib OPTIONAL)

abs-repr/tests/regression/verifier-passes/parsing/check-exit-nodes/test-parsing-exit-nodes.cpp

@@ -0,0 +1,96 @@
+/*******************************************************************************
+ *
+ * ARBOS pass for verifiying exit nodes in an AR function.
+ *
+ * Authors: Nija Shi
+ *
+ * Contact: ikos@lists.nasa.gov
+ *
+ * Notices:
+ *
+ * Copyright (c) 2011-2016 United States Government as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All Rights Reserved.
+ *
+ * Disclaimers:
+ *
+ * No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF
+ * ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT LIMITED
+ * TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO SPECIFICATIONS,
+ * ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE,
+ * OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL BE
+ * ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF PROVIDED, WILL CONFORM TO
+ * THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN ANY MANNER, CONSTITUTE AN
+ * ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR RECIPIENT OF ANY RESULTS,
+ * RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR ANY OTHER APPLICATIONS
+ * RESULTING FROM USE OF THE SUBJECT SOFTWARE.  FURTHER, GOVERNMENT AGENCY
+ * DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING THIRD-PARTY SOFTWARE,
+ * IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES IT "AS IS."
+ *
+ * Waiver and Indemnity:  RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST
+ * THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL
+ * AS ANY PRIOR RECIPIENT.  IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS
+ * IN ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH
+ * USE, INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM,
+ * RECIPIENT'S USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD
+ * HARMLESS THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS,
+ * AS WELL AS ANY PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW.
+ * RECIPIENT'S SOLE REMEDY FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE,
+ * UNILATERAL TERMINATION OF THIS AGREEMENT.
+ *
+ ******************************************************************************/
+
+#include <iostream>
+
+#include <arbos/semantics/ar.hpp>
+
+using namespace arbos;
+
+namespace {
+
+static Option< std::vector< std::string > > list("list,L",
+                                                 "Function name and names of "
+                                                 "the exit nodes in this "
+                                                 "sequence: function, return, "
+                                                 "unreachable, unwind.");
+
+class CheckExitNodesPass : public Pass {
+public:
+  CheckExitNodesPass()
+      : Pass("check-exit-nodes", "Verifies exit nodes in an AR function.") {}
+  virtual ~CheckExitNodesPass() {}
+
+  virtual void execute(AR_Node_Ref< AR_Bundle > bundle) {
+    assert(list);
+    const std::vector< std::string >& v = list;
+    assert(v.size() == 4);
+    AR_Node_Ref< AR_Function > f = (*(*bundle).getFunctionByNameId(v[0]));
+    AR_Node_Ref< AR_Code > c = (*f).getFunctionBody();
+
+    AR_Node_Ref< AR_Basic_Block > exit_bb = (*c).getExitBlock();
+    AR_Node_Ref< AR_Basic_Block > unreachable_bb = (*c).getUnreachableBlock();
+    AR_Node_Ref< AR_Basic_Block > unwind_bb = (*c).getUnwindBlock();
+
+    if (exit_bb.getUID() == 0)
+      assert(v[1] == "null");
+    else
+      assert(v[1] == (*exit_bb).getNameId());
+
+    if (unreachable_bb.getUID() == 0)
+      assert(v[2] == "null");
+    else
+      assert(v[2] == (*unreachable_bb).getNameId());
+
+    if (unwind_bb.getUID() == 0)
+      assert(v[3] == "null");
+    else
+      assert(v[3] == (*unwind_bb).getNameId());
+
+    std::cout << "Test passed!" << std::endl;
+  }
+};
+}
+
+extern "C" Pass* init() {
+  return new CheckExitNodesPass();
+}

analyzer/CMakeLists.txt

@@ -174,6 +174,10 @@ add_library(branching-opt SHARED src/ar-passes/branching_opt.cpp)
 target_link_libraries(branching-opt ${ARBOS_LIB} ${Boost_LIBRARIES})
 install(TARGETS branching-opt DESTINATION lib OPTIONAL)
 
+add_library(unify-exit-nodes SHARED src/ar-passes/unify_exit_nodes.cpp)
+target_link_libraries(unify-exit-nodes ${ARBOS_LIB} ${Boost_LIBRARIES})
+install(TARGETS unify-exit-nodes DESTINATION lib OPTIONAL)
+
 # analysis passes
 add_library(analyzer SHARED src/ar-passes/analyzer.cpp)
 target_link_libraries(analyzer ${ARBOS_LIB} ${GMPXX_LIB} ${GMP_LIB} ${SQLITE3_LIB} ${Boost_LIBRARIES})

analyzer/README.md

@@ -334,16 +334,10 @@ This folder contains classes that check for properties on the code (out-of-bound
    * backward abstract interpreter
   The backward abstract interpreter is limited to dataflow analyses, otherwise although sound it will be too imprecise.
 
-`include/analyzer/ikos-wrapper/domains_traits.hpp`: extend IKOS abstract domains with some extra functionality.
-
 ##### include/analyzer/domains
 
 This folder contains analysis-specific abstract domains not available in ikos core library.
 
-`include/analyzer/domains/value_domain.hpp`: this is a core abstract domain used for most of the analyses. This implements a value analysis 'a la' Mine.
-   * class `pointer_domain` extends an arbitrary numerical abstract domain to reason about pointer offsets.
-   * class `memory_domain` extends `pointer_domain` to reason about memory contents. For more precision, it uses also the nullity and uninitialized abstract domains.
-
 ##### include/analyzer/utils
 
 Common utilities for the analyses.