符号执行与运行时 API

本页的四个头文件提供了编译后的 C* 文件所用的运行时接口。cstarccstarc 翻译一个 .c.c 文件时，生成的是另一个 C 程序，并非证明对象。这个程序在运行时驱动符号执行引擎执行原始代码，检查各项契约，随后静默退出或报告验证失败的位置。它的所有操作都通过调用这里声明的函数完成。

这套接口只有一部分供证明代码使用，例如证明块中的 cst_get_symbolic_statecst_get_symbolic_state，以及手写证明库函数中的 ENSURE_OKENSURE_OK 宏，下文会逐条介绍。其余部分包括引擎生命周期、AST 构造和追踪记录，供编译器在翻译后的语句周围插桩使用，证明代码从不调用。用户只会在错误消息中遇到这些内容，本页也只介绍这一用途，其余内容由工具链的开发者文档说明。

symexec.hsymexec.h 是引擎头文件，声明了读取与改写符号状态、生成验证报告、打印与纯化断言的几个函数。在一条横幅注释之后，它还声明了 AST 构造器 API，供 cstarccstarc 将翻译后的程序传入引擎。证明块开始执行时，引擎已经在运行：启动与关闭引擎的生命周期调用由编译器写入生成的 mainmain 函数，证明代码从不调用它们。

它还声明了三个不透明 typedef（partial_programpartial_program、expressionexpression、ctypectype），以及两个位置结构体 locationlocation 和 rangerange。一个 rangerange 包含起止两个 locationlocation 和一个文件名，用来标明生成文件中的每个调用点对应用户源码的哪一段。

符号状态是引擎在当前程序点认为成立的断言，由描述堆的 hprophprop 与作用域内的纯事实合取而成。它和其他项一样，证明块通过下面五个函数访问它。

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.

有些程序点没有符号状态，例如 returnreturn 之后，因此需要 cst_check_symbolic_statecst_check_symbolic_state 来检查。在这些位置调用 cst_get_symbolic_statecst_get_symbolic_state 会使进程退出；先调用 cst_check_symbolic_statecst_check_symbolic_state，LSP 守护进程等调用方就能跳过该字段并继续执行。cst_pretty_symbolic_statecst_pretty_symbolic_state 是错误报告器使用的打印函数。由于调用它时已经在报告错误，它在设计上保证不会失败，也不会留下错误状态。

引擎产生的义务并非都在产生之处卸除。安全性附加条件与推迟的证明目标会被收集起来，在运行结束时打印，同时列出这次运行要求读者信任的全部内容。

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 将收集到的义务渲染为一个含三个数组的 JSON 对象。cstarc verifycstarc verify 打印的文档（同时保存在 _verif/<file>.vc_verif/<file>.vc 中），以及编辑器集成在文件作用域行读取的 vcvc 字段，内容都是这个对象。

verification_conditionsverification_conditions 保存引擎未能解决的蕴含，每条附带来源行号。axiomsaxioms 按加入顺序列出引擎启动之后理论新增的所有公理，包括证明块中的一次 new_axiomnew_axiom、SMT 求解器判定成立的目标，以及证明库假设而未证明的桥接引理。strategiesstrategies 按注册顺序列出用 cst_add_strategy_to_headercst_add_strategy_to_header 注册的策略文件，每项包含从 1 开始的序号和文件名；运行时自带的 common.strategiescommon.strategies 不在其中。证明代码可以通过两个访问函数遍历这份列表。只有三个数组都为空，一次运行才算通过验证。内存安全附加条件始终会被报告，无法通过开关隐藏。验证条件生成页说明这些条件从何而来，以及如何阅读输出。

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 是分离逻辑断言的标准渲染器。符号状态转储、验证条件与 LSP 输出都通过它渲染，因此各处使用的表示方式一致。渲染在 HOL Light 服务器上完成，只需一次往返通信（见HOL API：理论与定理页的 cst_assertion_stringcst_assertion_string）。

cst_purify_entailmentcst_purify_entailment 接受以文本给出的蕴含，包括前件、后件，以及绑定其自由变量的作用域名称，对它运行引擎的纯化策略，并返回剩余的待证目标。用 cst_add_strategy_to_headercst_add_strategy_to_header 注册的策略文件通过这一机制发挥作用；用策略纯化蕴含页说明策略文件包含什么，以及其中的展开、折叠与消去规则如何驱动这次调用。

引擎不抛出异常。几乎每个调用都会设置一个状态，调用方需要检查该状态。cstarccstarc 生成的验证程序会在每条语句之后检查一次；状态不是 OK 时，就会打印错误报告和追踪记录中的源码位置（见下文的 proof_trace.hproof_trace.h）。cstarc verify --debugcstarc verify --debug 会启用程序段转储，输出每个传入引擎的程序段。错误消息指向的语句若与预期不符，可以使用这个开关。

头文件中 AST builder APIAST builder API 横幅之后的全部内容都供编译器使用，包括 make_*make_* 构造器和将构造好的程序段传入引擎的调用。cstarccstarc 通过这些构造器向引擎描述翻译后的程序，证明代码从不调用它们。

许多引擎调用与证明器调用都接受列表，元素可以是项、定理、项配对或字符串。C 没有列表字面量，因此运行时提供了五个可变参数宏，用来从一组参数构造列表。生成的代码大量使用这些宏，手写证明代码也可以使用；这是传递列表最清楚的方式。这些宏随运行时一同发布，不属于任何证明库，因此无需额外链接其他库。

#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__)

每个宏都用复合字面量计算长度，即 sizeof((term[]){...}) / sizeof(term)sizeof((term[]){...}) / sizeof(term)，再将长度和各个参数一同传给一个可变参数后端函数。实际构造列表的是下面五个后端函数：

proof_util.hproof_util.h 为证明库代码提供支持，声明了各库函数使用的错误处理宏，以及构造消息所用的字符串辅助函数。与本页其余部分不同，它专门面向手写代码，例如操作体、glgl 函数或用户证明库中的辅助函数。

证明器客户端既不抛出异常，也不返回错误码。每个调用都会设置一个状态和一条消息，分别通过 get_last_status()get_last_status() 和 get_last_error()get_last_error() 读取。若某个函数连续调用三个证明器原语，就必须在每次调用后检查状态；状态不是 OK 时，该次调用取得的返回值就没有意义。

逐一手写这些检查十分繁琐，因此证明库函数采用一套固定的写法：先声明结果变量，然后执行各个步骤，在每一步后调用检查宏，最后以两个标号收尾：

thm my_rule(term tm) {
  thm result = empty_theorem;
  ASSUME_OK();                       // 若已有错误挂起，则拒绝开始
  thm h = ASSUME(tm);
  ENSURE_OK("my_rule: ASSUME failed on %s", cstr_term(tm));
  result = ...;
  ENSURE_OK("");                     // 沿用被调用函数自己的消息
  return result;
err:                                 // 某一步失败：记录后顺次落入
  ERR_FUN_PUTS("my_rule", cstr_term(tm));
def:                                 // 默认出口：状态已经设好
  return empty_theorem;
}

thm my_rule(term tm) {
  thm result = empty_theorem;
  ASSUME_OK();                       // 若已有错误挂起，则拒绝开始
  thm h = ASSUME(tm);
  ENSURE_OK("my_rule: ASSUME failed on %s", cstr_term(tm));
  result = ...;
  ENSURE_OK("");                     // 沿用被调用函数自己的消息
  return result;
err:                                 // 某一步失败：记录后顺次落入
  ERR_FUN_PUTS("my_rule", cstr_term(tm));
def:                                 // 默认出口：状态已经设好
  return empty_theorem;
}

两个标号的作用不同。某一步失败并记录错误之后，程序会跳转到 err:err:，将本函数的名称和参数追加到错误链中。def:def: 是默认出口：若进入函数时已有尚未处理的错误，ASSUME_OKASSUME_OK 会跳转到这里；从 err:err: 继续执行也会到达这里。两条路径都返回本函数的空值，并保留已设置的状态，供调用方的 ENSURE_OKENSURE_OK 检查。

这些宏的分工也与上述两条路径对应。ASSUME_OKASSUME_OK 在入口检查状态，已有错误时跳转到 defdef。ENSURE_OKENSURE_OK 与 ENSURE_CONDENSURE_COND 检查某一步，失败时记录一条消息并跳转到 errerr。CHECK_OK_OR_RETCHECK_OK_OR_RET 与 CHECK_OK_OR_GOTOCHECK_OK_OR_GOTO 用于错误恢复：它们清除状态并从正常出口退出，适用于失败在预期之内且已经得到处理的步骤。TRY_BEGINTRY_BEGIN / TRY_ENDTRY_END 划定一段区域，其中的错误只累积而不打印，使策略可以尝试某个操作，并在退出尝试时不输出错误消息。

#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.

上面的每条消息都由 gc_sprintfgc_sprintf 构造，插入消息的各个值则由相应的 cstr_*cstr_* 打印函数渲染。两者都在由垃圾回收管理的堆上分配内存，因此构造消息后无需手动管理其内存。两者也都保证不会失败，因为错误处理路径本身不能再出错。

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.

这些打印函数覆盖证明器客户端使用的各种对象类型，每个函数都生成带颜色的渲染结果，可以直接插入消息：

这些宏所依赖的函数与颜色宏，包括 try 状态管理、错误记录函数和 ANSI 包装宏，都属于运行时内部。证明代码使用宏，不直接调用底层函数。

一次验证失败涉及两个位置：失败的证明步骤，以及该步骤正在检查的用户源码位置。proof_trace.hproof_trace.h 将两者关联起来，其输出会出现在工具链打印的每条错误报告中。报告引擎错误时，错误消息下方有一行 near:near:，引用引擎当时正在执行的语句，并用 ▸▸ 标出引擎停止时到达的词法单元。接下来是若干 at file:line:colat file:line:col 行：先列出失败的语句，再按从内到外的顺序，为每次 glgl 函数活动列出一行并附上参数，最后用 in fin f 标明所在的 C* 函数。验证条件生成页给出了一份完整的报告。

产生这些输出的 API 调用由编译器生成：验证程序在每条证明语句和每个传入引擎的程序段周围记录位置，为每次 glgl 函数活动压入一个栈帧，运行时的错误报告器再根据这些记录生成栈回溯。证明代码不调用其中的任何函数，本页也不介绍它们的声明。

symexec.hsymexec.h 提供引擎接口，其中五个函数操作符号状态，遵循“读取—证明—提交”规范，其他功能包括生成验证报告、打印与纯化断言；生命周期调用和横幅之后的 make_*make_* 构造器供编译器使用，证明作者无需调用。proof_runtime.hproof_runtime.h 提供列表构造子，生成的代码与手写代码都用它们传递参数。proof_util.hproof_util.h 为手写证明代码提供错误处理规范，包括状态检查、err:err: / def:def: 这一对标号，以及用于填充消息内容的打印函数；这些函数在 GC 堆上分配内存。proof_trace.hproof_trace.h 则将这些消息关联到用户源码。

这四个头文件涵盖了生成的 C 文件除实际推理之外的全部工作；推理本身由证明器客户端负责。