Symbolic Execution and Runtime API

The four headers on this page are the runtime surface of a compiled C* file. When cstarccstarc translates a .c.c file it does not produce a proof object; it produces another C program — one that, when run, drives the symbolic execution engine over the original code, checks the contracts, and either exits quietly or reports where verification failed. Everything that program does, it does by calling functions declared here.

Only part of that surface is meant for proof code: cst_get_symbolic_statecst_get_symbolic_state in a proof block, and the ENSURE_OKENSURE_OK macro in a hand-written proof-library function. That part is documented below, entry by entry. The rest — engine lifecycle, AST construction, trace bookkeeping — is instrumentation the compiler emits around the translated statements, and proof code never calls it; it is mentioned here only where a user meets it, in an error message, and is otherwise the subject of the toolchain’s own developer documentation.

symexec.hsymexec.h is the engine header. It declares the handful of functions that read and rewrite the symbolic state, the verification report, the assertion printer and purification, and — behind a banner comment — the AST-builder API through which cstarccstarc feeds the translated program to the engine. The engine is already running when a proof block executes: the lifecycle calls that start it and shut it down are emitted by the compiler into the generated mainmain, and proof code never calls them.

It also declares three opaque typedefs (partial_programpartial_program, expressionexpression, ctypectype) and the two location structs locationlocation and rangerange. A rangerange is a start and end locationlocation plus a filename; it is how every call site in a generated file names the piece of user source it came from.

The symbolic state is the assertion the engine believes at the current program point: an hprophprop describing the heap, conjoined with the pure facts in scope. It is a term like any other, and a proof block gets at it through these five functions.

term cst_get_symbolic_state(void);

term cst_get_symbolic_state(void);

Gets the current symbolic state.

• returns — A term for the symbolic state.
• raises — Exits if the symbolic state is unavailable, e.g., after a return statement.
• raises — Returns empty_termempty_term and sets error status if cannot parse.

bool cst_check_symbolic_state(void);

bool cst_check_symbolic_state(void);

Checks whether a symbolic state is currently available.

• returns — truetrue if cst_get_symbolic_statecst_get_symbolic_state would succeed, otherwise falsefalse.

term cst_get_symbolic_state_with_exists(void);

term cst_get_symbolic_state_with_exists(void);

Gets the current symbolic state, with existential binders added properly.

• returns — A term for the symbolic state.
• raises — Exits if the symbolic state is unavailable, e.g., after a return statement.
• raises — Returns empty_termempty_term and sets error status if cannot parse.

void cst_set_symbolic_state(thm th);

void cst_set_symbolic_state(thm th);

Transforms the symbolic state according to the given entailment theorem. This employs a few tactics to rearrange the frames.

• th — The heap entailment theorem.
• raises — Exits if the symbolic state is unavailable, e.g., after a return statement, or the set state cannot be parsed.
• raises — Sets error status if the given theorem is not a entailment, the theorem has hypotheses, or the antecedent does not match the current symbolic state.

const char* cst_pretty_symbolic_state(const char* raw);

const char* cst_pretty_symbolic_state(const char* raw);

Renders a symbolic state captured as engine text (_get_symbolic_state_get_symbolic_state) the way assertions are shown elsewhere (the LSP dump, the VCs).

• raw — The state as engine text, or NULL.
• returns — The rendered assertion, or NULL if rawraw is empty or the prover cannot parse/print it.

cst_check_symbolic_statecst_check_symbolic_state exists because there are program points with no state at all — after a returnreturn, most obviously. Calling cst_get_symbolic_statecst_get_symbolic_state there exits the process; calling cst_check_symbolic_statecst_check_symbolic_state first lets a caller such as the LSP daemon skip the field and carry on. cst_pretty_symbolic_statecst_pretty_symbolic_state is the printer used by the error reporter, and is deliberately built never to fail or to leave an error status behind: it runs while a failure is already being reported.

Not every obligation the engine raises is discharged where it arises. Safety side conditions and postponed proof goals are collected and printed at the end of the run, together with everything the run has asked the reader to trust.

const char* cst_print_vc(void);

const char* cst_print_vc(void);

Renders verification and trust obligations as a JSON object with verification_conditionsverification_conditions, axiomsaxioms, and strategiesstrategies arrays. Strategy entries contain an index and filename; built-in strategies are excluded. Axioms added since cst_main_entry's baseline are reported in addition order.

• returns — The rendered verification-conditions text (GC-managed).

size_t cst_get_strategy_count(void);

size_t cst_get_strategy_count(void);

Gets the number of strategy trust obligations, excluding the runtime's built-in strategies. Repeated registrations count separately.

const char* cst_get_strategy(size_t i);

const char* cst_get_strategy(size_t i);

Gets a strategy trust obligation's filename in registration order.

• i — The zero-based index.
• returns — The recorded filename (GC-managed), or NULL if out of bounds.

cst_print_vccst_print_vc renders the collected obligations as a JSON object with three arrays — the document cstarc verifycstarc verify prints (and leaves in _verif/<file>.vc_verif/<file>.vc), and the vcvc field the editor integration reads at a file-scope line.

verification_conditionsverification_conditions holds the entailments the engine could not close, each with the source line it came from. axiomsaxioms holds every axiom the theory acquired after the engine started, in the order they were added: a new_axiomnew_axiom in a proof block, a goal an SMT solver validated, a bridge lemma a proof library assumed rather than proved. strategiesstrategies names each strategy file registered with cst_add_strategy_to_headercst_add_strategy_to_header, with a one-based index and the file name, in registration order; the runtime’s own common.strategiescommon.strategies is not listed. The two accessor functions walk that list from proof code. A run counts as verified only when all three arrays are empty. The memory-safety side conditions are always reported; there is no switch that hides them. Verification Condition Generation explains where these conditions come from and how to read the output.

const char* cst_print_assertion(term tm);

const char* cst_print_assertion(term tm);

Serialize a HOL separation-logic assertion for the active engine. Rendered by the prover server in one RPC (cst_assertion_stringcst_assertion_string); the in-client walk that used to do it (one RPC per term node) is still compiled in and can be selected with CST_PRINT_ASSERTION_LOCAL=1CST_PRINT_ASSERTION_LOCAL=1, or run alongside as a differential check with CST_PRINT_ASSERTION_CHECK=1CST_PRINT_ASSERTION_CHECK=1 (any difference prints both renderings and aborts). Exits on a term the printer cannot render, as it always has.

char* cst_purify_entailment(const char* ant, const char* con, int num_scope,
                            char** scopes);

char* cst_purify_entailment(const char* ant, const char* con, int num_scope,
                            char** scopes);

Run the active engine's entailment-purification strategy.

cst_print_assertioncst_print_assertion is the canonical renderer for separation-logic assertions: the symbolic-state dumps, the verification conditions and the LSP output all go through it, so what you read in one place is spelled the same way in the others. The rendering itself happens on the HOL Light server in one round trip (cst_assertion_stringcst_assertion_string on HOL API: Theories and Theorems).

cst_purify_entailmentcst_purify_entailment runs the engine’s purification strategy over an entailment given as text — antecedent, consequent, and the scope names that bind its free variables — and returns the residual goal. This is the machinery behind the strategy files registered with cst_add_strategy_to_headercst_add_strategy_to_header; Purifying Entailments with Strategies describes what a strategy file contains and how the unfold, fold and cancel rules inside it drive this call.

The engine does not throw. Nearly every call sets a status that the caller is expected to check, and the verifier that cstarccstarc emits checks it after every statement; a status that is not OK is what becomes the error report, printed together with the source location the trace recorded (see proof_trace.hproof_trace.h below). cstarc verify --debugcstarc verify --debug turns on the dump of each program segment as it is fed to the engine, which is the switch to reach for when an error names a statement you did not expect.

Everything after the header’s AST builder APIAST builder API banner exists for the compiler — the make_*make_* builders through which cstarccstarc describes the translated program to the engine, and the call that feeds a built segment in — and is never called from proof code.

Many engine and prover calls take a list — a list of terms, of theorems, of term pairs, of strings. C has no list literal, so the runtime supplies five variadic macros that build one from an argument list. Emitted code uses them constantly; hand-written proof code may use them too, and they are the clearest way to pass a list. They ship with the runtime rather than with any proof library, so nothing further has to be linked to use them.

#define TERM_LIST(...)                                                    \
  term_list_n(sizeof((term[]){__VA_ARGS__}) / sizeof(term) __VA_OPT__(, ) \
                                                  __VA_ARGS__)

#define TERM_LIST(...)                                                    \
  term_list_n(sizeof((term[]){__VA_ARGS__}) / sizeof(term) __VA_OPT__(, ) \
                                                  __VA_ARGS__)

#define THM_LIST(...)                                                  \
  thm_list_n(sizeof((thm[]){__VA_ARGS__}) / sizeof(thm) __VA_OPT__(, ) \
                                                __VA_ARGS__)

#define THM_LIST(...)                                                  \
  thm_list_n(sizeof((thm[]){__VA_ARGS__}) / sizeof(thm) __VA_OPT__(, ) \
                                                __VA_ARGS__)

#define TERM_PAIR_LIST(...)                             \
  term_pair_list_n(sizeof((term_pair[]){__VA_ARGS__}) / \
                   sizeof(term_pair) __VA_OPT__(, ) __VA_ARGS__)

#define TERM_PAIR_LIST(...)                             \
  term_pair_list_n(sizeof((term_pair[]){__VA_ARGS__}) / \
                   sizeof(term_pair) __VA_OPT__(, ) __VA_ARGS__)

#define STRING_LIST(...)                                                      \
  string_list_n(sizeof((char*[]){__VA_ARGS__}) / sizeof(char*) __VA_OPT__(, ) \
                                                     __VA_ARGS__)

#define STRING_LIST(...)                                                      \
  string_list_n(sizeof((char*[]){__VA_ARGS__}) / sizeof(char*) __VA_OPT__(, ) \
                                                     __VA_ARGS__)

#define CONST_STRING_LIST(...)                               \
  const_string_list_n(sizeof((const char*[]){__VA_ARGS__}) / \
                      sizeof(const char*) __VA_OPT__(, ) __VA_ARGS__)

#define CONST_STRING_LIST(...)                               \
  const_string_list_n(sizeof((const char*[]){__VA_ARGS__}) / \
                      sizeof(const char*) __VA_OPT__(, ) __VA_ARGS__)

Each macro computes its length from a compound literal — sizeof((term[]){...}) / sizeof(term)sizeof((term[]){...}) / sizeof(term) — and forwards it with the arguments to a variadic backend. Those five backends are the functions that do the work:

proof_util.hproof_util.h is the support header for proof-library code: the error-handling macros that every library function is written around, and the string helpers those functions use to build messages. Unlike the rest of this page it is aimed squarely at hand-written code — an operation body, a glgl function, a helper in a user proof library.

The prover client never throws and never returns an error code. Instead every call leaves a status behind, readable through get_last_status()get_last_status(), together with a message readable through get_last_error()get_last_error(). A function that calls three prover primitives in a row must check the status after each one, and the value it received in the meantime is meaningless if the status is not OK.

Writing those checks by hand is unbearable, so proof-library functions follow a fixed shape instead. The function declares its result variable, runs its steps with a checking macro after each, and ends with two labels:

thm my_rule(term tm) {
  thm result = empty_theorem;
  ASSUME_OK();                       // refuse to start with an error pending
  thm h = ASSUME(tm);
  ENSURE_OK("my_rule: ASSUME failed on %s", cstr_term(tm));
  result = ...;
  ENSURE_OK("");                     // propagate the callee's own message
  return result;
err:                                 // a step failed: record and fall through
  ERR_FUN_PUTS("my_rule", cstr_term(tm));
def:                                 // the default exit: status already set
  return empty_theorem;
}

thm my_rule(term tm) {
  thm result = empty_theorem;
  ASSUME_OK();                       // refuse to start with an error pending
  thm h = ASSUME(tm);
  ENSURE_OK("my_rule: ASSUME failed on %s", cstr_term(tm));
  result = ...;
  ENSURE_OK("");                     // propagate the callee's own message
  return result;
err:                                 // a step failed: record and fall through
  ERR_FUN_PUTS("my_rule", cstr_term(tm));
def:                                 // the default exit: status already set
  return empty_theorem;
}

Two labels, two meanings. err:err: is where a failed step jumps after the failure has been recorded, and it is the place to append the function’s own name and arguments to the error trail. def:def: is the bare default exit — reached by ASSUME_OKASSUME_OK when the function was entered with an error already pending, and fallen into from err:err:. Both return the function’s empty value, leaving the status set so the caller’s own ENSURE_OKENSURE_OK sees it.

The macros divide along the same lines. ASSUME_OKASSUME_OK guards the entry and jumps to defdef. ENSURE_OKENSURE_OK and ENSURE_CONDENSURE_COND check a step and jump to errerr, recording a message on the way. CHECK_OK_OR_RETCHECK_OK_OR_RET and CHECK_OK_OR_GOTOCHECK_OK_OR_GOTO are the recovering forms: they clear the status and take a normal exit, for a step whose failure is expected and handled. TRY_BEGINTRY_BEGIN / TRY_ENDTRY_END bracket a region in which errors accumulate silently instead of printing, so that a strategy may attempt something and back out without noise.

#define NOT_OK (get_last_status() != HOL_STATUS_OK)

#define NOT_OK (get_last_status() != HOL_STATUS_OK)

Macro to check if the last status is not OK.

• returns — True if the last status is not OK, false otherwise.

#define IN_TRY (proof_is_in_try() == true)

#define IN_TRY (proof_is_in_try() == true)

Macro to check if currently inside a try block.

• returns — True if inside a try block, false otherwise.

#define TRY_BEGIN() proof_try_begin()

#define TRY_BEGIN() proof_try_begin()

Macro to mark the beginning of a try block.

#define TRY_END() proof_try_end()

#define TRY_END() proof_try_end()

Macro to mark the end of a try block.

#define SET_OK()          \
  do {                    \
    set_status_error(""); \
    set_status_ok();      \
    proof_clear_errors(); \
  } while (0)

#define SET_OK()          \
  do {                    \
    set_status_error(""); \
    set_status_ok();      \
    proof_clear_errors(); \
  } while (0)

Macro to set the last status to OK.

#define PUTS_ERR(...)                                  \
  do {                                                 \
    if (IN_TRY) {                                      \
      proof_accumulate_error(gc_sprintf(__VA_ARGS__)); \
    } else {                                           \
      log_caught_error(__VA_ARGS__);                   \
    }                                                  \
  } while (0)

#define PUTS_ERR(...)                                  \
  do {                                                 \
    if (IN_TRY) {                                      \
      proof_accumulate_error(gc_sprintf(__VA_ARGS__)); \
    } else {                                           \
      log_caught_error(__VA_ARGS__);                   \
    }                                                  \
  } while (0)

Macro to print an error message, and if inside a try block, accumulate the error message instead of printing it immediately.

#define ASSUME_OK()                        \
  do {                                     \
    if (NOT_OK) {                          \
      PUTS_ERR_LAST("ASSUME_OK failed: "); \
      goto def;                            \
    }                                      \
  } while (0)

#define ASSUME_OK()                        \
  do {                                     \
    if (NOT_OK) {                          \
      PUTS_ERR_LAST("ASSUME_OK failed: "); \
      goto def;                            \
    }                                      \
  } while (0)

Macro to assume the last status is OK, and if not, print the last error message and goto a defdef label.

#define CHECK_OK_OR_RET(val)                                     \
  do {                                                           \
    if (NOT_OK) {                                                \
      log_trace("depress previous error: %s", get_last_error()); \
      set_status_ok();                                           \
      return val;                                                \
    }                                                            \
  } while (0)

#define CHECK_OK_OR_RET(val)                                     \
  do {                                                           \
    if (NOT_OK) {                                                \
      log_trace("depress previous error: %s", get_last_error()); \
      set_status_ok();                                           \
      return val;                                                \
    }                                                            \
  } while (0)

Macro to check if the last status is OK, and if not, depress previous error and return a specified value.

• val — The value to return if the last status is not OK.

#define CHECK_OK_OR_GOTO(lab)                                    \
  do {                                                           \
    if (NOT_OK) {                                                \
      log_trace("depress previous error: %s", get_last_error()); \
      set_status_ok();                                           \
      goto lab;                                                  \
    }                                                            \
  } while (0)

#define CHECK_OK_OR_GOTO(lab)                                    \
  do {                                                           \
    if (NOT_OK) {                                                \
      log_trace("depress previous error: %s", get_last_error()); \
      set_status_ok();                                           \
      goto lab;                                                  \
    }                                                            \
  } while (0)

Macro to check if the last status is OK, and if not, depress previous error and goto a specified label.

• lab — The label to goto if the last status is not OK.

#define ENSURE_OK(msg, ...)                                                   \
  do {                                                                        \
    if (NOT_OK) {                                                             \
      PUTS_ERR_LAST("ENSURE_OK failed: ");                                    \
      if ((msg)[0] != '\0')                                                   \
        set_status_error_and_record_msg(gc_sprintf(RED(msg), ##__VA_ARGS__)); \
      goto err;                                                               \
    }                                                                         \
  } while (0)

#define ENSURE_OK(msg, ...)                                                   \
  do {                                                                        \
    if (NOT_OK) {                                                             \
      PUTS_ERR_LAST("ENSURE_OK failed: ");                                    \
      if ((msg)[0] != '\0')                                                   \
        set_status_error_and_record_msg(gc_sprintf(RED(msg), ##__VA_ARGS__)); \
      goto err;                                                               \
    }                                                                         \
  } while (0)

Macro to check if the last status is OK, and if not, print the last error message, record a specified error message and goto the errerr label.

• msg — The error message to record if the last status is not OK, it can be a format string with variadic arguments.
• ... — The variadic arguments for the error message format string.

#define ENSURE_COND(cond, msg, ...)                                           \
  do {                                                                        \
    if (!(cond)) {                                                            \
      PUTS_ERR_LAST("ENSURE_COND failed: ");                                  \
      if ((msg)[0] != '\0')                                                   \
        set_status_error_and_record_msg(gc_sprintf(RED(msg), ##__VA_ARGS__)); \
      goto err;                                                               \
    }                                                                         \
  } while (0)

#define ENSURE_COND(cond, msg, ...)                                           \
  do {                                                                        \
    if (!(cond)) {                                                            \
      PUTS_ERR_LAST("ENSURE_COND failed: ");                                  \
      if ((msg)[0] != '\0')                                                   \
        set_status_error_and_record_msg(gc_sprintf(RED(msg), ##__VA_ARGS__)); \
      goto err;                                                               \
    }                                                                         \
  } while (0)

Macro to check a condition, and if not satisfied, print the last error message, record a specified error message and goto the errerr label.

• cond — The condition to check.
• msg — The error message to record if the condition is not satisfied, it can be a format string with variadic arguments.
• ... — The variadic arguments for the error message format string.

#define ERR_FUN_PUTS(func, ...)                          \
  do {                                                   \
    err_fun_puts(func __VA_OPT__(, ) __VA_ARGS__, NULL); \
  } while (0)

#define ERR_FUN_PUTS(func, ...)                          \
  do {                                                   \
    err_fun_puts(func __VA_OPT__(, ) __VA_ARGS__, NULL); \
  } while (0)

Macro to append a message to the error log with the function name and variadic arguments.

• func — The function name.
• ... — The variadic arguments of the message, should be a list of strings.

Every message above is built with gc_sprintfgc_sprintf, and every value spliced into one is rendered by a cstr_*cstr_* printer. Both allocate on the garbage-collected heap, so a message may be built and forgotten without bookkeeping, and neither ever fails — an error path must not itself be able to fail.

char* gc_sprintf(const char* fmt, ...);

char* gc_sprintf(const char* fmt, ...);

Formats a string with the given format and arguments with GC_MALLOC.

• fmt — The format string.
• ... — The variadic arguments for the format string.
• returns — A pointer to the formatted string.
• raises — Never fails.

char* gc_strcat(const char* s1, const char* s2);

char* gc_strcat(const char* s1, const char* s2);

Concatenates two strings.

• s1 — The first string.
• s2 — The second string.
• returns — A pointer to the concatenated string.
• raises — Never fails.

The printers cover the object types the prover client traffics in, each producing a colorized rendering suitable for dropping straight into a message:

The functions and color macros underneath these — the try-state plumbing, the error recorders, the ANSI wrappers — are runtime-internal; proof code reaches for the macro, never for the function below it.

A verification failure has two locations: the proof step that failed, and the place in the user’s source that step was checking. proof_trace.hproof_trace.h is what connects them, and its output appears in every error report the toolchain prints. Below the message, an engine error carries a near:near: line quoting the statement the engine was executing, with a ▸▸ marker at the token it had reached when it stopped; then come the at file:line:colat file:line:col lines — the failing statement first, then one line per glgl-function activation with its arguments, innermost first, and finally in fin f naming the enclosing C* function. Verification Condition Generation shows a complete report.

The API behind that output is emitted by the compiler: the generated verifier records a location around every proof statement and every fed program segment, pushes a frame for every glgl-function activation, and the runtime’s error reporter turns those records into the trace. None of it is called from proof code, and its declarations are not documented here.

symexec.hsymexec.h is the engine: five functions over the symbolic state governed by the read-prove-commit discipline, the verification report, the assertion printer and purification; the lifecycle calls and the make_*make_* builders behind its banner are the compiler’s, not the proof author’s. proof_runtime.hproof_runtime.h supplies the list constructors that both emitted and hand-written code pass arguments with. proof_util.hproof_util.h is the error-handling discipline hand-written proof code is built around: status checks, the err:err: / def:def: label pair, and the GC-allocated printers that fill in the messages. proof_trace.hproof_trace.h is why those messages point at user source.

Between them they account for everything a generated C file does apart from the actual inference — and the inference is the prover client’s job.