Public release version 3.3

Release date

March 2024

Summary

This is a maintenance release that addresses bugs related to Python dependencies, the order of passes in the LLVM frontend, and missing imports.

List of changes

analyzer

• Introduce compatibility with pygments >= 2.12 (#264).

Frontend

• Change order of passes (#205).

Core

• Add missing imports (#263).

Overall changes

• Version bump (#266).

Metrics

4 issues were closed as part of IKOS 3.3.

The net balance including all files (e.g., code, docs) is that IKOS 3.3 is 4 lines bigger than the previous version.

We had submissions from 1 new author who had never submitted patches to IKOS before.

Full Changelog: v3.2...v3.3

Public Release 3.2

Release date

December 2023

Summary

This is a maintenance release that addresses bugs related to Python packaging, LLVM 14, IPv6 handling and multi OS support. Other changes focus on the documentation, the software engineering process and leveraging features offered by Github.

There are two notable changes:

• We've dropped support for Python 2.
• We've added CI jobs via Github actions, which should ensure that IKOS keeps working on supported platforms.

List of changes

Analyzer changes

• Fixed hang of IKOS server due to not listening on IPv6 (#158).
• Fixed exception on Windows when IKOS is executed from a different drive (#165).
• Fix incorrect argument -section in call to llvm-objdump by @lojikil (#199).
• Fixed installation issues related to Python (#243, #242, #233, #193, #185).
• Fixed error parsing the output of llvm-objdump in LLVM 14 (#203).
• Typo fixes (#227).

AR Changes

• Add missing include directives by @gitrj95 (#201).

Overall changes

• Added documentation to the troubleshooting guide regarding a bug in old versions of APRON (#78).
• Added documentation to the troubleshooting guide regarding lack of support for multi-threaded code (#124).
• Fix the unaligned pointer analysis check parameter in the README.md file by @asensi in (#222).
• Set up Continuous Integration to build for Mac and Linux (#223).
• Fixed over-reaching gitignore rules (#217).
• Created Github releases for all IKOS versions, and attached the release notes to them (#219).
• Bump Copyright years (#246, #249).
• Version bump (#255).
• Improved issue / milestone / release handling process (not reflected as a separate issue).
• Fixed homebrew formula (NASA-SW-VnV/homebrew-core#9).

Metrics

23 issues were closed as part of IKOS 3.2.

The net balance including all files (e.g., code, docs) is that IKOS 3.2 is 437 lines smaller than the previous version.

We had submissions from 4 new authors who had never submitted patches to IKOS before.

Full Changelog: v3.1...v3.2

public release version 3.1

IKOS version 3.1 release notes

Release date

December 2022

List of changes

LLVM frontend changes

• Upgrade LLVM from 9.0.x to 14.0.x

Analyzer changes

• Add option to trace the invariant during analysis.
• Fix issue detecting uses of uninitialized dynamically-allocated memory.
• Allow analysis of programs without debug information.
• Support producing reports in SARIF format.
• Support producing reports in JUnit format.
• Allow running ikos-scan without an HTTP server, outputting JSON.
• Update use of deprecated Python function isAlive.
• Small refactoring changes.

Overall changes

• Update installation instructions for Ubuntu 20.04.

public release version 3.0

IKOS version 3.0 release notes

Release date

December 2019

List of changes

IKOS Core changes

• Implemented a parallel fixpoint engine
• Implemented a partitioning abstract domain based on the values of a given integer variable
• Implemented a polymorphic memory abstract domain
• Fixed most abstract domains to be thread-safe
• Refactor the pointer and memory abstract domain interfaces

LLVM frontend changes

• Upgraded LLVM from 8.0.x to 9.0.x

Analyzer changes

• Implemented a parallel interprocedural and intraprocedural value analysis
• Add an option to enable abstract domain partitioning based on the returned value of a function

public release version 2.2

IKOS version 2.2 release notes

Release date

August 2019

List of changes

IKOS Core changes

• Fixed non-convergence issues in the fixpoint iterator
• Improved the precision of the modulo operator for the DBM domain
• Improved the weak topological order implementation
• Implemented the narrowing operator with a threshold

Analyzer changes

• Improved the analysis and checks of the standard library functions
• Implemented a logger showing the progress of the analysis
• Added intrinsics to model library functions
• Added a checker to watch memory writes at a given location
• Added a checker to warn about unsound statements
• Added checks for recursive calls
• Forward -I, -D, -W, -w and -m flags to clang
• Support the analysis of LLVM text assembly file .ll
• Added an option to disable the cache of fixpoints
• Added options to control the fixpoint engine

LLVM frontend changes

• Upgraded LLVM from 7.0.x to 8.0.x
• Improved the support of LLVM debug information
• Improved the error message for mismatch of intrinsics
• Added support for empty array fields in structures

CMake changes

• Added support for linking with LLVM shared libraries
• Added version detection for GMP, MPFR, PPL, SQLite

Overall changes

• Added several sections to the documentation:
  • Analysis assumptions
  • Modeling library functions
  • Analysis of embedded software

public release version 2.1

IKOS version 2.1 release notes

Release date

December 2018

List of changes

IKOS Core changes

• Fixed a non-convergence issue in the fixpoint iterator

LLVM frontend changes

• Upgraded LLVM from 4.0.x to 7.0.x

Ikos-Scan changes

• Implemented ikos-scan, a tool to analyze a whole C/C++ project using IKOS

Overall changes

• Added support for Windows using the MinGW compiler

public release version 2.0

IKOS version 2.0 release notes

Release date

October 2018

List of changes

IKOS Core changes

• Updated the directory structure:
  • Renamed algorithms to adt;
  • Renamed iterator to fixpoint;
  • Added subdirectories under domain and value for each group of domains;
  • Added a legacy folder with unmaintained code. It will be removed in the future.
• Improved abstract domain interfaces using CRTP. Removed all the abstract domain traits.
• Added generic traits:
  • DumpableTraits to dump an object on a stream, for debugging purpose;
  • IndexableTraits to get a unique index representing an object;
  • GraphTraits to traverse a graph. It replaces the previous control flow graph API.
• Added a faster implementation of Patricia trees.
• Added machine integer abstract domains.
• Added unit tests using Boost.Test.
• Implemented a new pointer constraints system solver, previously called pta.
• Implemented machine_int::PolymorphicDomain, a machine integer abstract domain using runtime polymorphism that allows to use different abstract domains at runtime.
• Implemented machine_int::NumericDomainAdapter, a machine integer abstract domain wrapping a numeric abstract domain.
• Added abstract domain operators to perform widening with a threshold.
• Added a flow-sensitive context-sensitive pointer analysis in ValueDomain.

Analyzer changes

• Moved most of the implementation from the header files into the src directory.
• Remove the --ikos-pp option. It is recommended not to use optimizations.
• Added the --domain option, to choose the numerical abstract domain at runtime.
• Added the --hardware-addresses option, for software using Direct Memory Access (DMA).
• Added the --argc option, to specify the value of argc during the analysis.
• Added support for global variable dynamic initialization.
• Added support for the volatile keyword.
• Fix exception propagation analysis for C++.
• Added ikos/analyzer/intrinsic.h, a header file with IKOS intrinsics.
• Improved database writes by creating a new transaction every 8192 queries.
• Updated the output database schema to store more information about the source code.
• Improved the uninitialized variable analysis.
• Added a pass to find widening hints.
• Improved warning and error messages using LLVM debug information.
• Implemented several checks:
  • signed and unsigned integer overflow (sio, uio);
  • invalid shift count (shc);
  • pointer overflow (poa);
  • invalid pointer comparison (pcmp);
  • invalid function call (fca);
  • dead code (dca);
  • double free and lifetime analysis (dfa);
  • unsound analysis (sound).

AR changes

• Implemented a new Abstract Representation, based on the design of LLVM. The main changes are:
  • Improved memory management using clear ownership. The context owns types, a bundle owns functions, etc;
  • Added isa<>, cast<> and dyn_cast<> utilities, à la LLVM;
  • Added integer signedness information in the type system;
  • Added overflow and wrapping behaviours for integer operations;
  • Added visitors for statements and values;
  • Added intrinsics functions;
  • Added support for the volatile attribute;
  • Added traceability utilities, allowing to attach debug information to an AR object.
• Added a static type checker.
• Removed the branching-opt pass and added the simplify-cfg pass, a simpler version.
• Added the simplify upcast comparison pass.

LLVM frontend changes

• Added 3 different optimization levels in ikos-pp (none, basic and aggressive)
• Implemented a new translation from LLVM to Abstract Representation (AR). The main changes are:
  • In memory translation instead of writing into a file;
  • Attach LLVM debug information to AR;
  • Recover integer signedness information from debug information and several heuristics.
• Added the ikos-import tool. It translates LLVM bitcode into AR, useful for debugging.
• Added regression tests for the new translation from LLVM to AR.

CMake changes

• Add a target check that builds and runs all the tests.

Ikos-View changes

• Added ikos-view, a web interface to examine IKOS results.

Overall changes

• Updated the naming convention.

public release version 1.3

IKOS version 1.3 release notes

Release date

October 2017

List of changes

IKOS Core changes

• Added an implementation of the Gauge domain.
• Combined the memory domain and the pointer domain, improving the precision for arrays of pointers and virtual tables.
• Improved the documentation

Analyzer changes

• Added a report generator. The analyzer can now export the results in a gcc-style format, json or csv.
• Added an analysis of unaligned pointers.
• Improved the analysis performance by keeping previous fixpoints of called functions in memory.
• Added the intrinsic function __ikos_debug(), that dumps the current invariant.
• Added support for analyzing variable argument functions (va_start, va_arg, va_end and va_copy).
• Added support for analyzing structures in register (insertelement and extractelement in LLVM).
• Fixed an unsoundness in the exception analysis.
• Added a settings and times table in the result database, allowing a user to query the analysis options and timing results.
• Added special checks that warn about dangerous code patterns (such as casts from integers to pointers).
• Fixed and improved the analysis of bitwise and conversion operators.
• Moved all global variable initializations into the internal function __ikos_init_globals, also fixing the initialization of global objects in C++.

ARBOS changes

• Added support for C variable-length arrays (VLA).

LLVM frontend changes

• Upgraded to LLVM 4.0.x

public release version 1.2

IKOS version 1.2 release notes

Release date

October 2016

List of changes

IKOS Core changes

• Added an abstract domain to handle C++ exceptions.

Analyzer changes

• Implemented a proper C++ exception propagation handling using abstract interpretation. IKOS correctly handles C++ code with exceptions.
• Improved the analysis of string-related functions (such as strlen, strcpy and strcat).
• Fixed the precision of the null dereference analysis.

ARBOS changes

• Removed AR_Unwind as it is no longer generated by LLVM since LLVM 3.1
• Added APIs to set and retrieve the "resume" basic block in an AR_Code.

public release version 1.1.2

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