TESLA
Workflow
Once you have built TESLA, you need to either install it to your PATH or else set two environment variables:
The TESLA workflow deviates from a more typical LLVM-based workflow in that it adds two steps:
- analysis of all C sources, generating .tesla files, followed by
- instrumentation of LLVM IR, based on all .tesla files, generating instrumented IR.
This overall workflow is pictured below:
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:
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:
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:
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.