符号执行与运行时 API

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

其中一部分函数是证明代码直接调用的：证明块里的 cst_get_symbolic_statecst_get_symbolic_state、用来推迟一项 义务的 cst_add_axiom_to_headercst_add_axiom_to_header、手写证明库函数里的 ENSURE_OKENSURE_OK 宏。大多数则不是—— 它们是插桩，随翻译后的语句一同生成，在生成的 C 文件中成百上千地出现。两类都有文档， 因为阅读一份生成文件，或者阅读它输出的错误消息，都需要知道它们的含义。

因此下面每个条目都按调用者标注。当整块声明只供编译器使用时，就整体命名并列出名称， 而不逐个函数记录。

symexec.hsymexec.h 是引擎头文件。它声明了包夹一次验证运行的生命周期调用、少数几个读取与改写 符号状态的函数、验证条件与公理接口、错误报告器，以及——在一条横幅注释之后——cstarccstarc 借以把翻译后的程序送进引擎的 AST 构造器 API。

它还声明了三个不透明 typedef（partial_programpartial_program、expressionexpression、ctypectype），以及贯穿本页 与 proof_trace.hproof_trace.h 的两个位置结构体 locationlocation 和 rangerange。一个 rangerange 由起止两个 locationlocation 加上一个文件名构成；生成文件中的每个调用点都用它来标明自己来自用户源码的 哪一段。

三个调用包夹一次运行，三者都由 cstarccstarc 生成到 mainmain 函数之中。手写的证明代码从不 调用它们：证明块开始执行时，引擎早已启动。

void cst_main_entry(bool restore_server_on_exit);

void cst_main_entry(bool restore_server_on_exit);

The main entry of CStar. Should call before everything else.

• bool — restore_server_on_exit A flag to indicate whether to restore the HOL server on exit.
• raises — Exits with non-zero code if failed.

void cst_main_exit(void);

void cst_main_exit(void);

The main exit of CStar. Should call before returning from main.

void cst_symbolic_engine_init(void);

void cst_symbolic_engine_init(void);

Initializes the symbolic execution engine. Should call before any symbolic execution related operations.

cst_main_entrycst_main_entry 接受一个标志，决定进程退出时是否回滚 HOL Light 服务器的理论状态—— 头文件的 @param@param 行把参数的类型和名称一起写了出来，所以上面那一条读起来有些别扭。 cst_symbolic_engine_initcst_symbolic_engine_init 之所以单列，是因为证明器连接与符号执行引擎是两项不同的 服务：只操作项与定理的运行需要前者，而不需要后者。

符号状态是引擎在当前程序点所相信的断言：一个描述堆的 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 是错误报告器所用的打印函数，它被刻意设计成永不失败、也不 留下错误状态：它运行的时候，某个失败已经在报告之中了。

引擎提出的义务并非都在提出之处卸除。安全性附加条件与推迟的证明目标会被收集起来，在 运行结束时打印，而 cst_add_axiom_to_headercst_add_axiom_to_header 正是证明有意推迟某项义务的手段。

const char* cst_print_vc(void);

const char* cst_print_vc(void);

Renders the verification conditions as a JSON object with a verification_conditionsverification_conditions array and an axiomsaxioms array.

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

int cst_set_ignore_unsafe_vc_flag(bool flag);

int cst_set_ignore_unsafe_vc_flag(bool flag);

Toggles if printing safety verification conditions.

• flag — Ignore or not.
• returns — zero.

bool cst_check_ignore_unsafe_vc_flag(void);

bool cst_check_ignore_unsafe_vc_flag(void);

Checks if printing safety verification conditions.

• returns — truetrue if ignoring safety verification conditions, otherwise falsefalse.

thm cst_add_axiom_to_header(term tm);

thm cst_add_axiom_to_header(term tm);

A user-side wrapper for creating a temporary axiom that intended to be proved later.

• tm — The term for the axiom.
• returns — A theorem for the axiom.
• raises — Returns empty_theoremempty_theorem and sets error status if tmtm is not of :bool:bool type.

int cst_get_axiom_count(void);

int cst_get_axiom_count(void);

Gets the number of axioms to be proved.

• returns — The number of axioms to be proved.

term cst_get_axiom_to_be_prove(int i);

term cst_get_axiom_to_be_prove(int i);

Gets the i-th axiom to be proved.

• i — The index of the axiom.
• returns — The term for the i-th axiom to be proved.
• raises — Returns a truetrue term if ii is out of bounds.

cst_print_vccst_print_vc 把收集到的全部内容渲染为一个 JSON 对象，其中含一个 verification_conditionsverification_conditions 数组和一个 axiomsaxioms 数组——cstarc --vccstarc --vc 与编辑器集成所消费的 正是这一格式。ignore-unsafe 标志控制是否包含内存安全附加条件；它由命令行设置，而检查 函数让生成的代码可以查询它。 验证条件生成页说明这些条件从何而来，以及 如何阅读输出。

cst_add_axiom_to_headercst_add_axiom_to_header 是逃生出口。它不加证明就把一个项变成定理，把该项记录为一项 未了义务，并让运行继续下去；事后可以用 cst_get_axiom_countcst_get_axiom_count 与 cst_get_axiom_to_be_provecst_get_axiom_to_be_prove 遍历这份列表。公理列表非空的一次运行，并不是一份完成的 证明。

const char* cst_print_assertion(term tm);

const char* cst_print_assertion(term tm);

Serialize a HOL separation-logic assertion for the active engine.

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 输出 都经过它，因此在一处读到的写法，在别处也是同样的写法。

cst_purify_entailmentcst_purify_entailment 对以文本给出的蕴含——前件、后件，以及约束其自由变量的作用域 名称——运行引擎的纯化策略，并返回残余的待证目标。这正是用 cst_add_strategy_to_headercst_add_strategy_to_header 注册的策略文件背后的机制；用策略纯化蕴含页 说明策略文件包含什么，以及其中的展开、折叠与消去规则如何驱动这次调用。

引擎不抛异常。几乎每个调用都会设置一个状态，并要求调用方检查；生成的验证程序在它所 生成的每条语句之后都会检查一次。

void cst_exit_on_error(void);

void cst_exit_on_error(void);

Exits the program if get_last_status()get_last_status() is not OK, reporting the error and, under it, wherever the trace says it happened.

• loc — Unused; the trace carries the location. See cst_exit_on_error_with_loccst_exit_on_error_with_loc.
• raises — Exits if the last status is not OK.

void cst_exit_on_error_with_loc(range ran);

void cst_exit_on_error_with_loc(range ran);

If error, exits with the given location string for error reporting.

• ran — The location range for error reporting.
• raises — Exits if the last status is not OK.

void cst_record_last_loc_for_report(const char* loc);

void cst_record_last_loc_for_report(const char* loc);

Records the last location for reporting purposes.

• loc — The location string to record.

void cst_set_debug(bool debug);

void cst_set_debug(bool debug);

Set the runtime debug flag used when feeding program texts to the symbolic engine. The generated program calls this once at startup with its CST_DEBUG value.

• debug — Whether to print each fed header segment.

bool cst_check_debug(void);

bool cst_check_debug(void);

Check the runtime debug flag.

• returns — Whether the debug flag is set.

cst_exit_on_errorcst_exit_on_error 就是编译器生成的那次检查：若最近一次状态不是 OK，它会把错误连同 追踪记录下的位置一起打印出来，然后退出。它的文档注释仍然记录着一个 locloc 参数，而 声明中已经不再接受这个参数——位置现在来自 proof_trace.hproof_trace.h，而不再来自实参， cst_exit_on_error_with_loccst_exit_on_error_with_loc 则是显式给出 rangerange 的旧形式。 cst_record_last_loc_for_reportcst_record_last_loc_for_report 是与之配套的设置函数，供那些只有位置字符串、没有 rangerange 的代码路径使用。

两个调试函数控制程序段送入引擎时是否输出追踪。生成的程序在启动时用自身 CST_DEBUGCST_DEBUG 宏的值调用一次 cst_set_debugcst_set_debug，因此 cstarc -DCST_DEBUG=1cstarc -DCST_DEBUG=1 无需重新编译运行时即可 打开程序段转储。

int cst_checkpoint(void);

int cst_checkpoint(void);

Checkpoint the server's theory state. Returns an id for cst_restore.

void cst_restore(int id);

void cst_restore(int id);

Roll the server's theory state back to a cst_checkpoint id.

• raises — Fails if the given id is invalid.

void cst_resume(void);

void cst_resume(void);

Rebuild the prover connection after cst_checkpoint_fork(). Does NOT touch libsac (its state is already in memory).

• raises — Fails if cannot re-initialize the prover connection.

这三个是原型，由 LSP 守护进程使用，并非面向证明代码。一次验证运行会同时在两个地方累积 状态：引擎进程内的符号状态，以及 HOL Light 服务器的全局理论状态。要从证明中途的某一点 恢复，就必须把两者一起捕获下来，因此守护进程为服务器建立检查点，并通过 fork()fork() 以 写时复制的方式冻结引擎的内存。证明器连接不是 fork 安全的，所以要在 fork 之前断开， 之后在两侧各自重建——cst_resumecst_resume 做的就是这次重建。这套接口预计还会变动。

头文件中 AST builder APIAST builder API 横幅之后的全部内容，都是为了让 cstarccstarc 能把一个待符号执行 的程序交给引擎。编译器遍历它正在翻译的 C 源码，为每个构造生成一次调用，把该构造重建 为引擎侧的 AST 结点：类型用 make_int_type()make_int_type()，表达式用 make_binary_expr(...)make_binary_expr(...)，循环头 用 make_while_condition(...)make_while_condition(...)，契约子句用 make_cst_require(...)make_cst_require(...)。这些结果被串接 起来，再推入引擎。

make_unary_exprmake_unary_expr、make_binary_exprmake_binary_expr、make_assignmake_assign 与 make_inc_decmake_inc_dec 的 int opint op 参数 取自头文件在这些构造器上方声明的四个枚举：bin_opbin_op（十八个二元运算符，从 BINOP_MULTIPLYBINOP_MULTIPLY 到 BINOP_LOGICAL_ORBINOP_LOGICAL_OR）、assign_opassign_op（普通赋值与十种复合赋值形式）、 unary_opunary_op（UNOP_ADDRESSUNOP_ADDRESS、UNOP_DEREFUNOP_DEREF、算术正负号，以及两种取反）与 incdec_opincdec_op （前置与后置的自增和自减）。这些参数的类型写作 intint 而不是相应的枚举，因此生成的文件 中显示的是数值常量。

还有两条声明属于同一内部层次。cst_feed_program_segment_with_loccst_feed_program_segment_with_loc 是真正把构造好的 程序段连同其来源 rangerange 一起推入引擎的调用——它是上面这一切在生成代码一侧的对应物。 MEMSTREAM_TO_GCMEMSTREAM_TO_GC 是运行时内部使用的便捷宏，用于把某个打印函数的输出捕获成一个受垃圾 回收管理的字符串；它打开一个内存流，运行宏体，再把结果复制到 GC 堆上。

许多引擎调用与证明器调用都接受一个列表——项的列表、定理的列表、项配对的列表、字符串 的列表。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("ASSUME_OK failed: %s", get_last_error()); \
      goto def;                                           \
    }                                                     \
  } while (0)

#define ASSUME_OK()                                       \
  do {                                                    \
    if (NOT_OK) {                                         \
      PUTS_ERR("ASSUME_OK failed: %s", get_last_error()); \
      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("ENSURE_OK failed: %s", get_last_error());                     \
      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("ENSURE_OK failed: %s", get_last_error());                     \
      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("ENSURE_COND failed: %s", get_last_error());                   \
      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("ENSURE_COND failed: %s", get_last_error());                   \
      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 状态的底层管道（proof_try_beginproof_try_begin、proof_try_endproof_try_end、proof_is_in_tryproof_is_in_try）、错误记录 函数（proof_accumulate_errorproof_accumulate_error、proof_flush_errorsproof_flush_errors、proof_clear_errorsproof_clear_errors、 set_status_error_and_record_msgset_status_error_and_record_msg、err_putserr_puts、err_fun_putserr_fun_puts）、strip_ansi_colorstrip_ansi_color， 以及 ANSI 颜色码与包装宏，都属于运行时内部：它们的存在是为了让上面那些宏得以写出， 而证明代码应当使用宏，不要去用底下的函数。

一次验证失败有两个位置：失败的那个证明步骤，以及该步骤正在检查的用户源码位置。 proof_trace.hproof_trace.h 就是把两者连接起来的东西。生成的验证程序用位置记录包夹每一条证明语句， 为每次 glgl 函数的活动连同其参数压入一个栈帧，并在失败时把累积的记录变成源码层面的 栈回溯：失败的语句、每次活动一行，以及外围的 C* 函数。

这让本头文件在本页中显得与众不同——它的输出被用户不断阅读，出现在工具链打印的每一条 错误消息里，而它的 API 只由生成的代码调用。项与定理这两类参数在调用时以裸句柄的形式 捕获，只是一次指针存储，不需要往返证明器；只有在确实要报告失败时才惰性地转成字符串， 因此在通过的路径上，这套插桩几乎不花代价。

第一块是 cstarccstarc 在证明块语句与 glgl 函数调用周围生成的内容。

void cst_record_last_stmt(range stmt, const char* text, const char* fn,
                          range fn_loc);

void cst_record_last_stmt(range stmt, const char* text, const char* fn,
                          range fn_loc);

Open a proof-block statement window: record the statement being run and the C* function that encloses the proof block.

• stmt — The statement's source range.
• text — The statement's source text.
• fn — The enclosing C* function's name.
• fn_loc — The proof block's source range.

void cst_record_gl_stmt(range stmt, const char* text);

void cst_record_gl_stmt(range stmt, const char* text);

Record the statement being run inside a gl function body.

• stmt — The statement's source range.
• text — The statement's source text.

void cst_frame_push(const char* fn);

void cst_frame_push(const char* fn);

Push a frame for a gl-function activation.

• fn — The gl function's name.

void cst_frame_arg_term(const char* name, term tm);

void cst_frame_arg_term(const char* name, term tm);

Record a term-valued argument of the innermost frame.

• name — The parameter's name.
• tm — The term handle; stringified only if a failure is reported.

void cst_frame_arg_thm(const char* name, thm th);

void cst_frame_arg_thm(const char* name, thm th);

Record a theorem-valued argument of the innermost frame.

• name — The parameter's name.
• th — The theorem handle; stringified only if a failure is reported.

void cst_frame_arg_int(const char* name, long long v);

void cst_frame_arg_int(const char* name, long long v);

Record an integer-valued argument of the innermost frame.

• name — The parameter's name.
• v — The value.

void cst_frame_arg_str(const char* name, const char* s);

void cst_frame_arg_str(const char* name, const char* s);

Record a string-valued argument of the innermost frame.

• name — The parameter's name.
• s — The value; borrowed, must outlive the activation.

void cst_frame_pop(void);

void cst_frame_pop(void);

Pop the innermost frame. A pop at depth 0 is a no-op.

第二块生成在程序语句周围——也就是送往符号执行引擎的、翻译后的用户代码，与在旁边 一同运行的证明步骤相对。

void cst_trace_note_program_stmt(range stmt, const char* text);

void cst_trace_note_program_stmt(range stmt, const char* text);

Note the program statement about to be fed to the symbolic engine.

• stmt — The statement's source range.
• text — The statement as the engine sees it; collapsed to one line.

void cst_trace_note_unlocated_stmt(const char* text);

void cst_trace_note_unlocated_stmt(const char* text);

Note a program segment that carries no source location (a header line the runtime synthesizes, say).

• text — The segment as the engine sees it.

void cst_trace_enter_function(const char* fn, range fn_loc);

void cst_trace_enter_function(const char* fn, range fn_loc);

Enter the C* function the following statements belong to.

• fn — The function's name.
• fn_loc — The range of the function's header.

void cst_trace_leave_function(void);

void cst_trace_leave_function(void);

Leave the current C* function.

头文件的第三块标记为运行时内部，这里不作记录：它是报告的那一侧——构造并打印栈回溯、 信号处理路径、TRYTRY 恢复所用的深度与截断钩子，以及重置。其中的函数由运行时自身的错误 报告器调用，生成的代码与手写代码都不会调用。

symexec.hsymexec.h 是引擎：三个生命周期调用，五个受“读取—证明—提交”规范约束、作用于符号状态 的函数，验证条件与公理接口，纯化，错误报告器，以及横幅之后那 74 个 make_*make_* 构造器——它们的存在是为了让编译器能把一个程序描述给引擎。proof_runtime.hproof_runtime.h 提供生成代码所需的列表构造子，且无需链接用户库。proof_util.hproof_util.h 是手写证明代码所围绕的 错误处理规范：状态检查、err:err: / def:def: 这一对标号，以及负责填充消息内容、在 GC 堆上 分配的打印函数。proof_trace.hproof_trace.h 则是那些消息能指向用户源码的原因。

四者合起来解释了一份生成的 C 文件除实际推理之外所做的一切——而推理是证明器客户端的 职责。