Your First C* Program

In this section, we will write and verify a C* function that computes an absolute value. This simple example shows how details of C’s semantics can lead to undefined behavior (UB). A basic goal of C program verification is to rule out undefined behavior; later tutorials will discuss memory safety and functional correctness in more detail. At the end of this section, we will download and configure C*‘s proof standard library, which supports common specifications and proofs and is used in the later examples.

1. Create a new folder: mkdir cstar_verification ; cd cstar_verificationmkdir cstar_verification ; cd cstar_verification.
2. Initialize the project: cstarc initcstarc init. This creates cstar.tomlcstar.toml and compile_flags.txtcompile_flags.txt.
3. Create the file .vscode/settings.json.vscode/settings.json with the following content:

{
  "clangd.path": "cst_clangd"
}

{
  "clangd.path": "cst_clangd"
}

4. Open the project in VSCode.
5. Open the command palette with ctrl+shift+pctrl+shift+p (or shift+cmd+pshift+cmd+p on macOS), then type and select CStar IDE: Start HOL Light ServerCStar IDE: Start HOL Light Server.

6. The server is ready when the HOL Light Server panel displays the following:

...
[INFO] Use Ctrl-\ to quit the server!
[INFO] RPC server listening on 127.0.0.1:7000 ..

...
[INFO] Use Ctrl-\ to quit the server!
[INFO] RPC server listening on 127.0.0.1:7000 ..

In the C* project you just created, add a new file abs.cabs.c with the following contents:

#cst_include "cstar.h"
int myabs(int x)
{
  int r;
  if (x >= 0) {
    r = x;
  } else {
    r = -x;
  }
  return r;
}

#cst_include "cstar.h"
int myabs(int x)
{
  int r;
  if (x >= 0) {
    r = x;
  } else {
    r = -x;
  }
  return r;
}

The #cst_include#cst_include on the first line imports a verification-time header. The symbols it defines are used only for program verification, such as proof functions for theorem proving, and cannot be used in implementation code. cstar.hcstar.h is C*‘s core header and primarily provides an interface to the HOL Light Server described above. We will explain how this header works when we start writing proof code. For now, every C* program must begin with #cst_include "cstar.h"#cst_include "cstar.h".

In VSCode, right-click on line 4 of the code and choose Show Symbolic StateShow Symbolic State: this C* verification feature displays the symbolic state at that line, which we will explain shortly. Here, VSCode reports an error on the corresponding line:

error: function without a specification
  near: int myabs(int x) ▸{
  at .../cstar_verification/abs.c:3:5  in myabs
  fed to the engine:
      int myabs(int x) {

error: function without a specification
  near: int myabs(int x) ▸{
  at .../cstar_verification/abs.c:3:5  in myabs
  fed to the engine:
      int myabs(int x) {

To verify a program, we must first write its specification. C* uses the common contract-style approach, specifying for each function:

• Precondition: the condition that the function’s inputs must satisfy.
• Postcondition: the condition that the function’s outputs should satisfy.

In C*, we write function contracts using the annotations [[cst::require(...)]][[cst::require(...)]] and [[cst::ensure(...)]][[cst::ensure(...)]]:

#cst_include "cstar.h"
int myabs(int x)
  [[cst::require(`emp`)]]
  [[cst::ensure(`
      fact(
        (x >= 0i && __return == x) ||
        (x <  0i && __return == --x)
      )
  `)]]
{
  int r;
  if (x >= 0) {
    r = x;
  } else {
    r = -x;
  }
  return r;
}

#cst_include "cstar.h"
int myabs(int x)
  [[cst::require(`emp`)]]
  [[cst::ensure(`
      fact(
        (x >= 0i && __return == x) ||
        (x <  0i && __return == --x)
      )
  `)]]
{
  int r;
  if (x >= 0) {
    r = x;
  } else {
    r = -x;
  }
  return r;
}

The backtick syntax `...``...` encloses logical expressions. C* uses separation logic for specifications, which we will discuss in detail later. In this example:

• empemp describes an empty heap. In this example, the function requires no caller-owned memory and returns no memory resources.

• fact()fact() requires the program state to satisfy . In myabsmyabs’s postcondition, it requires:

  • either the parameter xx is non-negative and the return value equals xx;
  • or the parameter xx is negative and the return value equals the negation of xx.

Now select Show Symbolic StateShow Symbolic State again from the right-click menu on line 11 (the opening brace at function entry). A symbolic-state panel appears on the right side of VSCode:

This too is a separation-logic expression: data_at data_at means that address stores a value of type . Separation logic describes resources: each block of memory that a program operates on must be described explicitly. The state above says that the address of variable xx stores an intint equal to xx’s value at function entry.

Next, select Show Symbolic StateShow Symbolic State from the right-click menu on line 12 to see:

The undef_data_atundef_data_at predicate is similar to data_atdata_at, but does not specify the stored value. Using the value of rr immediately after this declaration raises an error because the variable is uninitialized. The state also introduces ****, the separating conjunction of separation logic. The logical expression ** ** describes memory that can be split into two disjoint parts satisfying and , respectively. Here, it states that xx and rr occupy disjoint regions of memory. Later, we will use this property of separation logic to describe aliasing precisely and concisely.

If you view the symbolic state after the function returns (line 18), you get:

C* currently does not return a symbolic state at function exit. This is consistent with the reclamation of memory for parameters and local variables when the function returns.

Viewing the symbolic state already involves some verification. C* reports an error if a function has no specification, if we access memory whose resource has not been described, or if we use an uninitialized variable’s value. Advancing the symbolic state thus provides some evidence of memory safety. Verification must also consider functional correctness. If we view the symbolic state at the function’s closing brace (line 19), the panel shows a verification condition:

If all verification conditions hold, the function has no undefined behavior, is memory-safe, and behaves according to its contract. The condition above is reported at line 16, the assignment r = -x;r = -x;. It requires the symbolic state before |--|-- (entailment in separation logic) to entail the state after it. Here, we must show that if xx is negative at function entry, its value is not -2147483648-2147483648 (~~ denotes logical negation). This condition is false: an integer variable can take the value -2147483648-2147483648. The reason for this condition lies in C’s semantics: signed-integer overflow is undefined behavior, so negating -2147483648-2147483648 is undefined behavior. The state after |--|-- requires that negation does not cause undefined behavior.

To make our absolute-value function pass verification, we can strengthen the function’s precondition, constraining its input:

int myabs(int x)
  [[cst::require(`fact(x > --2147483648i)`)]]
  ...

int myabs(int x)
  [[cst::require(`fact(x > --2147483648i)`)]]
  ...

This restricts the input so that its absolute value can be computed correctly within the integer range. After making this change, view the symbolic state again at the end of the function. The panel shows:

We have now written and verified our first C* program. To see how verification detects an incorrect implementation, change r = -x;r = -x; on line 16 to r = x;r = x; and view the symbolic state again at the end of the function. The verification condition becomes:

When xx is negative at function entry, the code returns xx, but the specification requires the negation of xx. This leaves the unprovable condition x == -xx == -x. Verification can thus catch logical errors during development by checking that the implementation behaves according to its specification.

Before continuing to the later tutorials, set up C*‘s proof standard library in the project.

1. Make sure you are in the project root (cstar_verificationcstar_verification) and initialize git version control (via git initgit init).
2. Run git submodule add https://gitee.com/cstarlang/cstar_stdlib.git proofgit submodule add https://gitee.com/cstarlang/cstar_stdlib.git proof. Do not change the proofproof folder name!
3. Change the first line of abs.cabs.c from #cst_include "cstar.h"#cst_include "cstar.h" to #include "proof/proof.h"#include "proof/proof.h".
4. Try viewing the symbolic state in abs.cabs.c again to confirm it still works.

• Initialize a C* project with cstarc initcstarc init and start the HOL Light Server in VSCode; every C* program (after the C preprocessor) begins with #cst_include "cstar.h"#cst_include "cstar.h".
• Verification starts from a specification: C* adopts contract-style specifications, written with the annotations [[cst::require(...)]][[cst::require(...)]] and [[cst::ensure(...)]][[cst::ensure(...)]] for pre- and postconditions; in a contract, a variable name denotes its value at the function entry, and __return__return denotes the return value.
• Backticks `...``...` enclose logical expressions, whose syntax comes from HOL Light: integer constants carry an ii suffix, unary negation is ----, and logical negation is ~~.
• Show Symbolic StateShow Symbolic State displays the symbolic state at a line: data_atdata_at/undef_data_atundef_data_at explicitly describe each block of memory, and **** states that two parts of memory are disjoint.
• Verification conditions have the form “symbolic state |--|-- symbolic state”; if all hold, the function has no undefined behavior, is memory-safe, and behaves according to its contract. The myabsmyabs example shows how a verification condition exposes UB from signed-integer overflow and how strengthening the precondition rules it out.
• After setting up the proof standard library, use #include "proof/proof.h"#include "proof/proof.h" in place of #cst_include "cstar.h"#cst_include "cstar.h"; the later tutorials build on this library.