Your First C* Program

In this section we will write and verify our first C* program: computing an absolute value. Although this is a very simple example, as we will show, subtle points in C’s semantics can easily lead code into undefined behavior (UB); a basic goal of verifying C programs is to ensure the code is free of undefined behavior. In later tutorials we will further discuss how to ensure memory safety and functional correctness. Before finishing this section, we will download and configure C*‘s proof standard library, which provides support for common specifications and proofs; the later examples in this tutorial will also build on it.

1. Create a new folder: mkdir cstar_verification ; cd cstar_verificationmkdir cstar_verification ; cd cstar_verification.
2. Initialize the project: cstarc initcstarc init.
3. Edit the .vscode/settings.json.vscode/settings.json file:

{
  "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. When the HOL Light Server panel prints the following, the startup has succeeded!

...
[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 cannot be used in implementation code; they are only for program verification — for instance, the proof functions needed during theorem proving. cstar.hcstar.h is the core header provided by C*, and it mainly offers the interface to the HOL Light Server described above. We can ignore this line for now; we will explain its mechanism when we actually need to write proof code. For the moment, just remember that 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 is a verification feature provided by C* that displays the symbolic state at that line (explained shortly). However, we get an error (flagged as a diagnostic on the corresponding line in VSCode):

error: function without a specification
  at .../cstar_verification/abs.c:3:5  in myabs

error: function without a specification
  at .../cstar_verification/abs.c:3:5  in myabs

This tells us that to verify a program we must first write its specification. In C*, we adopt the widely used contract-style specification: at the granularity of a function, we provide:

• 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;
}

In the code above, we use the backtick syntax `...``...` to enclose logical expressions. In C*, we use separation logic as the specification logic; we will expand on this later. In the example above:

• empemp can be read, for now, as the truth value — it imposes no constraint on the program state.

• fact()fact() imposes on the program state the constraint expressed by . It is used in myabsmyabs’s postcondition, where the constraint is:

  • 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 right-click Show Symbolic StateShow Symbolic State again on line 11 (the opening brace at the function entry), and a symbolic-state panel appears on the right side of VSCode showing:

This too is a separation-logic expression: data_at data_at means a value of type is stored at address . This reflects that separation logic is a logic that characterizes resources: to describe a block of memory a program operates on, that memory resource must be described explicitly. The symbolic state above reads as “at the address of variable xx there is stored an intint equal to xx’s initial value at the function entry”.

Next, right-click Show Symbolic StateShow Symbolic State again on line 12, and we get the following symbolic state:

The undef_data_atundef_data_at predicate is similar in meaning to data_atdata_at, the difference being that the value stored in the memory it describes is indeterminate; thus, immediately using the value of rr afterward also raises an error, because it is an uninitialized variable. This symbolic state also introduces a logical connective ****, the very important separating conjunction of separation logic. The logical expression ** ** describes a memory space that can be split into two disjoint parts, satisfying and respectively. So the symbolic state above explicitly states that the variables xx and rr occupy different regions of memory. Later, we will also see that this capability of separation logic can be used to characterize aliasing precisely and concisely.

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

For now, C* does not return a symbolic state at the function exit; this is intuitive to some extent, because once a function returns, the memory it owned (parameters and local variables) is reclaimed.

When viewing the symbolic state, we are in fact already doing some verification: an error is raised if no function specification is written; an error is raised if we access memory whose resource has not been described; and an error is raised if we use the value of an uninitialized variable. Indeed, being able to advance the symbolic-state reasoning partly demonstrates memory safety; but program verification must also consider functional correctness. In fact, if we view the symbolic state at the closing brace of the function exit (line 19), the panel actually shows a verification condition:

The role of a verification condition is this: if all verification conditions hold, then the function has no undefined behavior, is memory-safe, and its behavior conforms to what the function contract describes. The verification condition above is reported at line 16, which is the assignment r = -x;r = -x;. It reads as: the symbolic state before |--|-- (the implication connective of separation logic) entails the symbolic state after it: if xx is negative at the function entry, then its value is not equal to -2147483648-2147483648 (the ~~ in a logical expression denotes logical negation). At first glance this seems odd, because the verification condition is clearly false: an integer variable can indeed take the value -2147483648-2147483648. But this is exactly the subtlety of C’s semantics: signed-integer overflow is undefined behavior, so negating -2147483648-2147483648 is undefined behavior. The part after |--|-- in the verification condition above is precisely meant to ensure that the negation operation does not trigger 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)`)]]
  ...

In other words, we require the function’s input to guarantee that the absolute value can be computed correctly within the integer range. After this change, view the symbolic state again at the position after the function ends, and the panel shows:

That is, we have finished writing and verifying our first C* program! Before ending this section, let us see what kind of verification condition appears when the implementation code is wrong. For example, change r = -x;r = -x; on line 16 to r = x;r = x;, view the symbolic state again at the end of the function, and the verification condition becomes:

This says that in the case where xx’s initial value at the function entry is negative, because we return xx rather than the negation of xx described in the specification, we end up with an unprovable verification condition x == -xx == -x. This shows that program verification can catch logical errors during development, ensuring that the implementation’s behavior conforms to the specification.

Before starting the later tutorials, let us 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 describe each block of memory resource explicitly, and **** says that two parts of memory are disjoint.
• Verification conditions have the form “symbolic state |--|-- symbolic state”; if all verification conditions hold, the function has no undefined behavior, is memory-safe, and functionally conforms to its contract. The myabsmyabs example shows how UB such as signed-integer overflow is exposed by a verification condition, and how it is fixed by strengthening the precondition.
• 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.