Symbolic Execution and Runtime API

The four headers on this page provide the runtime interface for a compiled C* file. When cstarccstarc translates a .c.c file, it produces another C program rather than a proof object. Running that program drives the symbolic execution engine over the original code, checks the contracts, and either exits quietly or reports where verification failed. The generated program performs these operations by calling functions declared here.

Only part of this interface is intended for proof code, such as cst_get_symbolic_statecst_get_symbolic_state in a proof block and the ENSURE_OKENSURE_OK macro in a hand-written proof-library function. These entries are documented below. The remaining calls manage the engine lifecycle, construct ASTs, and record traces. The compiler emits them around the translated statements, and proof code never calls them. This page describes them only as needed to explain error messages; further details belong in the toolchain’s developer documentation.

symexec.hsymexec.h is the engine header. It declares functions for reading and rewriting the symbolic state, generating the verification report, printing assertions, and purification. After a banner comment, it also declares 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 compiler emits the lifecycle calls that start and stop it 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 contains a start and end locationlocation and a filename. It identifies the portion of user source corresponding to each call site in a generated file.

The symbolic state is the assertion the engine holds at the current program point: an hprophprop describing the heap, conjoined with the pure facts in scope. It is a term like any other, accessible from a proof block 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 checks whether a symbolic state exists at a program point; for example, there is no state after a returnreturn. 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 continue. cst_pretty_symbolic_statecst_pretty_symbolic_state is the printer used by the error reporter. Because it runs while a failure is already being reported, it is designed never to fail or leave an error status.

The engine collects obligations that are not discharged where they arise. It prints safety side conditions and postponed proof goals at the end of the run, together with everything the run requires 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. This object is the document that cstarc verifycstarc verify prints and saves in _verif/<file>.vc_verif/<file>.vc, and the contents of the vcvc field that the editor integration reads at a file-scope line.

verification_conditionsverification_conditions holds the entailments the engine could not close, each with its source line. axiomsaxioms holds every axiom added to the theory after the engine started, in the order added: a new_axiomnew_axiom in a proof block, a goal an SMT solver validated, or a bridge lemma a proof library assumed rather than proved. strategiesstrategies lists 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 let proof code traverse this list. A run counts as verified only when all three arrays are empty. Memory-safety side conditions are always reported; no switch 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. Symbolic-state dumps, verification conditions, and LSP output all use it, so assertions have a consistent representation across these outputs. Rendering takes place 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 takes an entailment as text, consisting of the antecedent, consequent, and scope names that bind its free variables. It runs the engine’s purification strategy over the entailment and returns the residual goal. This call uses the strategy files registered with cst_add_strategy_to_headercst_add_strategy_to_header; Purifying Entailments with Strategies describes their contents and how their unfold, fold, and cancel rules guide purification.

The engine does not throw exceptions. Nearly every call sets a status that the caller is expected to check. The verifier that cstarccstarc emits checks it after every statement and, if the status is not OK, prints an error report with the source location recorded in the trace (see proof_trace.hproof_trace.h below). cstarc verify --debugcstarc verify --debug dumps each program segment as it is fed to the engine. Use this switch when an error names an unexpected statement.

Everything after the header’s AST builder APIAST builder API banner is intended for the compiler: the make_*make_* builders through which cstarccstarc describes the translated program to the engine, and the call that feeds a constructed segment into it. Proof code never calls these functions.

Many engine and prover calls take lists of terms, theorems, term pairs, or strings. C has no list literal, so the runtime supplies five variadic macros that build lists from their arguments. Generated code uses them frequently, and hand-written proof code can also use them to pass lists clearly. They are included in the runtime, so using them requires no additional proof library to be linked.

#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 the list length from a compound literal — sizeof((term[]){...}) / sizeof(term)sizeof((term[]){...}) / sizeof(term) — and passes it with the arguments to a variadic backend. These five backend functions construct the lists:

proof_util.hproof_util.h supports proof-library code with error-handling macros used by every library function and string helpers for building messages. It is intended specifically for hand-written code: an operation body, a glgl function, or a helper in a user proof library.

The prover client never throws exceptions or returns an error code. Instead, every call sets a status, readable through get_last_status()get_last_status(), and 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 call. If the status is not OK, that call’s return value is meaningless.

To avoid repeating these checks by hand, proof-library functions follow a fixed structure. 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;
}

The two labels serve different purposes. A failed step jumps to err:err: after recording the failure; the code at this label appends the function’s name and arguments to the error trail. def:def: is the default exit, reached by ASSUME_OKASSUME_OK when the function is entered with an error already pending, or by falling through from err:err:. Both paths return the function’s empty value and leave the status set for the caller’s ENSURE_OKENSURE_OK to check.

The macros implement these error-handling paths. ASSUME_OKASSUME_OK checks the status on entry and jumps to defdef if an error is pending. ENSURE_OKENSURE_OK and ENSURE_CONDENSURE_COND check a step and, on failure, record a message and jump to errerr. CHECK_OK_OR_RETCHECK_OK_OR_RET and CHECK_OK_OR_GOTOCHECK_OK_OR_GOTO support recovery: they clear the status and take a normal exit when a step’s failure is expected and handled. TRY_BEGINTRY_BEGIN / TRY_ENDTRY_END delimit a region in which errors accumulate without being printed, allowing a strategy to attempt an operation and abandon it without printing error messages.

#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 inserted into a message is rendered by a cstr_*cstr_* printer. Both allocate on the garbage-collected heap, so messages require no manual memory management. Neither ever fails, since the error-handling path must not itself 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 used by the prover client. Each produces a colorized rendering that can be inserted directly into a message:

The underlying functions and color macros for managing try-state, recording errors, and wrapping ANSI codes are internal to the runtime. Proof code uses the macros and never calls the underlying functions directly.

A verification failure has two locations: the proof step that failed and the place in the user’s source that the step was checking. proof_trace.hproof_trace.h connects them, and its output appears in every error report the toolchain prints. For an engine error, a near:near: line below the message quotes the statement the engine was executing, with a ▸▸ marker at the token it had reached when it stopped. The at file:line:colat file:line:col lines follow: 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 compiler emits the API calls that produce this output. The generated verifier records a location around every proof statement and every program segment fed to the engine, and pushes a frame for every glgl-function activation. The runtime’s error reporter constructs the trace from these records. Proof code never calls these functions, and their declarations are not documented here.

symexec.hsymexec.h provides five functions for accessing the symbolic state under the read-prove-commit discipline, along with verification reporting, assertion printing, and purification. Its lifecycle calls and the make_*make_* builders after the banner are intended for the compiler. proof_runtime.hproof_runtime.h supplies the list constructors used to pass arguments in both generated and hand-written code. proof_util.hproof_util.h supports error handling in hand-written proof code through status checks, the err:err: / def:def: label pair, and GC-allocated printers for messages. proof_trace.hproof_trace.h associates those messages with user source.

Together, these headers cover all operations performed by a generated C file except inference itself, which is handled by the prover client.