The FDR API¶

libfdr is a 64-bit only library available for C++, Java, and Python that exposes part of FDR’s internals to external tools. This API is designed to be stable, and we will endeavour to make backwards-incompatible changes only when absolutely necessary. libfdr currently exposes functionality that allows files to be loaded, particular assertions to be executed, counterexamples to be interrogated, and arbitrary expressions to be evaluated. As such, it exposes a strict superset of functionality as compared to the machine-readable output of the command-line interface.

As a simple example, the following python loads a file, executes all assertions, and then begins to inspect any counterexamples:

session = fdr.Session()
session.load_file("phils8.csp")

# Evaluate an expression
print session.evaluate_expression("<0,1>^<2,3>", None).result

# Run the assertions
for assertion in session.assertions():
    assertion.execute(None)

    for counterexample in assertion.counterexamples():
        debug_context = fdr.DebugContext(counterexample, True)
        debug_context.initialise(None);

        spec = debug_context.specification()
        impl = debug_context.implementation()

Full API documentation for the C++ version is available. Stub API documentation for the Java version is available. At the present time there is no full documentation available for the Java and Python APIs, however, the C++ documentation should be a suitable reference. In particular, the Python function names are identical, and the Java function names are simply converted into camel-case (e.g. node_path() becomes nodePath()).

If you are interested in additional functionality please contact us and describe the additional functionality that you would like.

Getting Started with C++¶

In order to use the C++ API, a C++11 compatible compiler, such as g++ 4.8, or clang++ 3.1 is required. The following file demonstrates the basics of using libfdr. Firstly, libfdr is initialised, then Session is created, into which the file phils8.csp is loaded. Lastly, all the assertions are executed.

#include <fdr/fdr.h>
#include <iostream>

int main(int argc, char** argv)
{
    FDR::library_init(&argc, &argv);

    try
    {
        FDR::Session session;
        session.load_file("phils8.csp");
        for (const std::shared_ptr<FDR::Assertions::Assertion>& assertion
                : session.assertions())
        {
            assertion->execute(nullptr);
            std::cout << assertion->to_string() << " "
                << (assertion->passed() ? "Passed" : "Failed");
        }
    }
    catch (const FDR::Error& error)
    {
        std::cout << error.what() << std::endl;
    }

    FDR::library_exit();

    return 0;
}

If FDR is installed at /opt/fdr (which it is by default on Linux), and the above file is saved as main.cc, then the file above can be compiled and linked using:

g++ -std=c++11 -I/opt/fdr/include -L/opt/fdr/lib -D_GLIBCXX_USE_CXX11_ABI=0
    -o libfdr_demo main.cc
    -Wl,-rpath=/opt/fdr/lib -lfdr

A more interesting example is included in API Examples. The C++ API is fully documented and is available here.

Note that all strings used by libfdr are UTF-8 encoded. The use of the boost.nowide is strongly recommended.

ABI Compatibility¶

Different C++ implementations are not always compatible with each other. Below, we list the compiler version that libfdr was compiled with, and also versions that it will be compatible with.

On Linux, libfdr was compiled with g++ 4.8. We believe that this should be compatible with all C++-11 compliant releases of g++. It should also be compatible with any other C++11 compliant compiler that also uses libstdc++.

On Mac OS X, libfdr was compiled using the system-provided clang++ using libc++ as the standard library. This means that when compiling under Mac OS X, the compiler flag -stdlib=libc++ must be used. Failure to do so will lead to various link errors.

On Windows, libfdr was compiled using g++ 4.8 using the mingw-w64 build with POSIX threads and Structured Exception Handling (SEH). Unfortunately, on Windows, compiler compatibility is currently very limited. We hope to provide ABI compatibility with MSVC at some point in the future.

Getting Started with Java¶

FDR also provides a Java interface, which was generated using SWIG and provides equivalent functionality to the C++ interface. In order to use the FDR Java interface, at least Java 1.6 is required. The following file gives a simple example of how the API can be used. This initialises FDR, loads the file phils8.csp, and then executes all of the assertions in the file.

import uk.ac.ox.cs.fdr.*;

package FDRDemo {

public static void main(String[] argv)
{
    try {
        Session session = new Session();
        session.loadFile("phils8.csp");
        for (Assertion assertion : session.assertions()) {
            assertion.execute(null);
            System.out.println(assertion.toString()+" "+
                (assertion.passed() ? "Passed" : "Failed"));
        }
    }
    catch (InputFileError error) {
        System.out.println(error);
    }
    catch (FileLoadError error) {
        System.out.println(error);
    }

    fdr.libraryExit();
}

}

The above example can be compiled and executed as follows, assuming that FDR has been installed into its usual location on Linux:

javac -classpath /opt/fdr/lib/fdr.jar FDRDemo.java
java -classpath /opt/fdr/lib/fdr.jar:. FDRDemo

A more interesting example is included in API Examples, and can be compiled in similar fashion. The Java API has stub documentation available here, and therefore the C++ documentation may also be useful to refer to.

Warning

Many of the classes contain a delete() method. This is considered an internal implementation detail, and as such should not be manually called. It is likely to be removed in a future release.

Getting Started with Python¶

FDR also provides a Python interface, which was generated using SWIG and provides equivalent functionality to the C++ interface. In order to use the FDR Python interface, at least Python 2.6 is required. The following file gives a simple example of how the API can be used. This initialises FDR, loads the file phils8.csp, and then executes all of the assertions in the file.

import os
import platform
import sys

if platform.system() == "Linux":
    for bin_dir in os.environ.get("PATH", "").split(":"):
        fdr4_binary = os.path.join(bin_dir, "fdr4")
        if os.path.exists(fdr4_binary):
            real_fdr4 = os.path.realpath(os.path.join(bin_dir, "fdr4"))
            sys.path.append(os.path.join(os.path.basename(os.path.basename(real_fdr4)), "lib"))
            break
elif platform.system() == "Darwin":
    for app_dir in ["/Applications", os.path.join("~", "Applications")]:
        if os.path.exists(os.path.join(app_dir, "FDR4.app")):
            sys.path.append(os.path.join(app_dir, "FDR4.app", "Contents", "Frameworks"))
            break

import fdr

fdr.library_init()

session = fdr.Session()
try:
    session.load_file("phils8.csp")
    for assertion in session.assertions():
        assertion.execute(None)
        print "%s: %s" % (assertion, "Passed" if assertion.passed() else "Failed")
catch FDRError, e:
    print e

fdr.library_exit()

The above example can be executed using python fdr_demo.py.

A more interesting example is included in API Examples, and can be executed in similar fashion.