This file describes the history of significant (e.g., user-visible) changes in Codex.
- While frontend
- New bitvector -> integer translation
- New string abstraction
- SVComp support
- New, more dynamic GUI
These bindings should be compatible with OCaml 5.1
We now have a flake.nix which makes things simpler.
With these functions, all calls now show in the Tracelog trace, easing understanding of what the analyzer does.
With an OCaml compiled to js backend that communicates with the native code using marshalled binary data.
This corresponds to the NSAD’2024 publication, and its (not yet published followup)
In particular when converting data from relational to the non-relational domain.
We generally create new names automatically when needed, but this process does not cover every case yet. The abstract domains do not yet fully take advantage of the fact that we can only point to names yet.
We now have a function -codex-analyze-functions to specify the list of functions to analyzer, and -codex-output-prefix to give an additional prefix of the output files (.html and .cdump)
This includes:
- Removing the “absence of length” case in arrays, the enum case
- Giving names to many “basic types” (though some, like bytes or integers, have no names because they cannot be pointed to)
- Supressing useless constructs like Constructor
- etc.
We have started some work to classify and categorize the alarms reported by the analysis. We now have a place to centralize all the alarms in Transfer_functions.Alarms
These appear in Memory_sig.ml.
This makes use of the new block abstraction, that can handle blocks of variable length.
Including but not limited to:
- Unifying of hashing functions
- Change of the queries interface
- Remove most of the warnings when compiling Codex
This follows the [NSAD’24] paper.
The trailing semicolon is no longer necessary. However, you can no longer use struct or union as a type name.
This covers only a the modules Transfer_functions and some toplevel documentation for now.
We now have a module at the bottom of the domain hierarchy (domains_constraints_overflow_check) that reports alarms when flags such as nsw, nuw, nusw are used. This allows intermediate modules (e.g., performing pointer arithmetics) to use these flags and receive an alarm in case of overflow.
This new type exists in addition to boolean, binary, and integer values. It roughly corresponds to an enum type in C. The main purpose of this type is to represent (in the abstract) a finite set of objects, that is enumerated precisely, unlike e.g. using intervals for the same thing.
This is useful notably when analyzing device drivers.
This version corresponds to the artefact published at OOPSLA’24.
Second released version.
This is the first released version.