符号执行与运行时 API

本页的四个头文件构成编译后的 C* 文件所面对的运行时界面。cstarccstarc 翻译一个 .c.c 文件时并不产生证明对象，而是产生另一个 C 程序——它运行起来会驱动符号执行引擎走过原始代码、检查各项契约，然后要么安静地退出，要么报告验证在何处失败。那个程序所做的一切，都是通过调用这里声明的函数完成的。

这套界面只有一部分是给证明代码用的：证明块里的 cst_get_symbolic_statecst_get_symbolic_state，以及手写证明库函数里的 ENSURE_OKENSURE_OK 宏。这一部分在下文逐条记录。其余部分——引擎生命周期、AST 构造、追踪记录——是编译器在翻译后的语句周围生成的插桩，证明代码从不调用；本页只在用户会遇到它们的地方（也就是错误消息里）提及，其余内容属于工具链自身的开发者文档。

symexec.hsymexec.h 是引擎头文件。它声明了少数几个读取与改写符号状态的函数、验证报告、断言打印与纯化，以及——在一条横幅注释之后——cstarccstarc 借以把翻译后的程序送进引擎的 AST 构造器 API。证明块开始执行时，引擎早已在运行：启动与关闭引擎的生命周期调用由编译器生成到 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.

cst_check_symbolic_statecst_check_symbolic_state 之所以存在，是因为有些程序点根本没有状态——最明显的就是 returnreturn 之后。在那里调用 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 横幅之后的全部内容都是编译器的输出——cstarccstarc 借以向引擎描述翻译后程序的 make_*make_* 构造器，以及把构造好的程序段送入引擎的那次调用——证明代码从不调用它们。

许多引擎调用与证明器调用都接受一个列表——项的列表、定理的列表、项配对的列表、字符串的列表。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 文件除实际推理之外所做的一切——而推理是证明器客户端的职责。