Computer Laboratory

TESLA

Workflow

Once you have built TESLA, you need to either install it to your PATH or else set two environment variables:

$ export PATH=$PATH:/path/to/tesla/scripts

The TESLA workflow deviates from a more typical LLVM-based workflow in that it adds two steps:

  1. analysis of all C sources, generating .tesla files, followed by
  2. instrumentation of LLVM IR, based on all .tesla files, generating instrumented IR.

This overall workflow is pictured below:

TESLA workflow

The TESLA workflow augments an LLVM-based C workflow.

On this page, we apply this workflow to a simple example: two C files foo.c and bar.c that are compiled into a binary:

Example workflow

A simple example of a TESLA workflow.

Analysis

In the analysis stage, TESLA is used to parse temporal assertions defined by the programmer as described in Programming with TESLA. To analyse source files foo.c and bar.c that require CFLAGS="-Wno-error -D VERSION=42", the programmer (or the build system) should run the following commands:

$ tesla analyse foo.c -o foo.tesla -- -Wno-error -D VERSION=42 $ tesla analyse bar.c -o bar.tesla -- -Wno-error -D VERSION=42 $ tesla cat foo.tesla bar.tesla -o tesla.manifest # combine into single manifest

The TESLA analyser needs to know the appropriate CFLAGS because it is running a full Clang parser on the C code, and errors, warnings, condititional compilation, etc. need to be consistent with those options used by Clang when compiling the source into LLVM IR.

Instrumentation

The LLVM instrumenter modifies LLVM IR, adding hooks for events that are named in a TESLA manifest. If once again CFLAGS="-Wno-error -D VERSION=42", the TESLA instrumenter is run as follows:

$ clang $CFLAGS foo.c -o foo.ll $ tesla instrument -tesla-manifest tesla.manifest foo.ll -o foo.instr.ll $ tesla instrument -tesla-manifest tesla.manifest bar.ll -o bar.instr.ll

Calls to instrumentation are inserted inline within LLVM basic blocks:

@@ -108,7 +202,9 @@ %3 = bitcast i8* %2 to i32*, !dbg !62 %4 = load i32* %3, align 4, !dbg !62 %add = add nsw i32 %4, 1, !dbg !62 + call void @__tesla_instrumentation_struct_field_store_struct.object.refcount(%struct.object* %0, i3 2 %add, i32* %3), !dbg !62 store i32 %add, i32* %3, align 4, !dbg !62 + call void @__tesla_instrumentation_callee_return_hold(%struct.object* %o) ret void, !dbg !63 }

These language-level events are translated by machine-generated instrumentation into symbols that can be consumed by TESLA automata:

define void @__tesla_instrumentation_callee_enter_hold(%struct.object*) { preamble: %1 = call i32 (...)* @tesla_debugging([13 x i8]* @debug_name) %2 = icmp ne i32 %1, 0 br i1 %2, label %printf, label %entry printf: ; preds = %preamble %3 = call i32 (i8*, ...)* @printf(i8* getelementptr inbounds ([20 x i8]* @8, i32 0, i32 0), %struct .object* %0) br label %entry entry: ; preds = %printf, %preamble br label %"example.c:51#2:instr" "example.c:51#2:instr": ; preds = %entry %key = alloca %tesla_key+ %4 = ptrtoint %struct.object* %0 to i64+ %5 = getelementptr inbounds %tesla_key* %key, i32 0, i32 0+ store i64 %4, i64* %5+ %6 = getelementptr inbounds %tesla_key* %key, i32 0, i32 4+ store i32 1, i32* %6+ %7 = call i32 @tesla_update_state(i32 1, i32 6, %tesla_key* %key, i8* getelementptr inbounds ([15 x i8]* @10, i32 0, i32 0), i8* getelementptr inbounds ([328 x i8]* @11, i32 0, i32 0), %tesla_transitions* @transitions4) %8 = icmp eq i32 %7, 0 br i1 %8, label %"example.c:85#8:instr", label %die "example.c:85#8:instr": ; preds = %"example.c:51#2:instr" %key1 = alloca %tesla_key %9 = ptrtoint %struct.object* %0 to i64 %10 = getelementptr inbounds %tesla_key* %key1, i32 0, i32 0 store i64 %9, i64* %10 %11 = getelementptr inbounds %tesla_key* %key1, i32 0, i32 4 store i32 1, i32* %11 %12 = call i32 @tesla_update_state(i32 1, i32 12, %tesla_key* %key1, i8* getelementptr inbounds ([1 5 x i8]* @42, i32 0, i32 0), i8* getelementptr inbounds ([684 x i8]* @43, i32 0, i32 0), %tesla_transi tions* @transitions24) %13 = icmp eq i32 %12, 0 br i1 %13, label %exit, label %die exit: ; preds = %"example.c:85#8:instr" ret void die: ; preds = %"example.c:85#8:instr", %"example.c:51#2 :instr" call void @tesla_die(i8* getelementptr inbounds ([42 x i8]* @9, i32 0, i32 0)) ret void }

These instrumentated .ll files can be linked together into the final binary (or shared library) using Clang. The result must be linked against libtesla, which provides the tesla_update_state() function.