文档描述
本文档为对ESBMC模型检测工具进行代码阅读随手写的文档，该文档针对工具ESBMC version 7.5.0 64-bit x86_64 linux 的BMC框架进行代码阅读，主要关注其BMC算法框架，数据结构以及如何从BMC得到的中间数据结构进行SMT编码的过程。本文档希望通过对以上问题的描述，让读者对ESBMC的流程有个清晰的认识，从而能够从代码层面理解其高效的原因，以及能够快速上手BMC框架进行修改和编程。
格式说明和注意事项
文档内的结构以代码层级缩进表示，其中对代码的未探究清楚的疑问以*这样的问题？*格式表示，对于已经解决的问题用**这样的问题?**格式表示， 序号层级为三层itemize，1.2.3., (1)(2)(3), a.b.c.
建议配合ESBMC源码食用
参考文献，文档和手册
- 对BMC算法有理论上的理解
- ESBMC的TSE文章
- ESBMCgithub repo上的latex写的manual
- github代码
- github原理讲解
ESBMC BMC代码精读
- ESBMC 入口文件 src/esbmc/main.cpp
-
parseoptions.main()
-
esbmc_parseoptionst::do_it(), do_it()做三件事情：
- get_command_line_options: 解析命令行CMD
- get_goto_functions: 根据读入的源文件，创建GOTO程序，并进行预处理
问题：此处预处理会进行什么操作？
此处的解析翻译流程是什么样的？
主要分为3步：create_goto_program, process_goto_program以及output_goto_program:
1. create_goto_program 根据用户输入的是否是binary来决定是直接读入goto_functions还是进行parse，如果是parse_goto_programs，其流程为
（1）首先调用parse(const cmdlinet &cmdline)来解析输入的命令行参数（language_ui.cpp）
（2）如果parse的内容是文件名, 直观理解利用 language_id_by_path 来确定文件的语言类型，如C,CPP等，并利用解析到的语言类型，创建 languaget 数据结构language，languaget为不同语言的解析接口，随后通过调用 language 的成员函数parse(file_name)来对输入的源文件进行解析，并将得到的goto_functionst数据结构传到引用
问题：如果以ansi_c为例子，具体的解析流程如何？
2. process_goto_program 根据注释描述，会对上一步得到的 goto_functions进行静态分析，并对在进行符号执行之前对goto_functions进行转换，这里的静态分析包括但不限于：区间分析，不可达代码去除，为k-induction进行预处理，applying GOTO contractors：
从代码层面来说，对goto_functions进行的操作有：
(1) remove_no_op
(2) remove_unreachable
(3) 应用algorithms算法：这里的 algorithms 算法是 esbmc_parseoptionst中用vector存的一个 goto_functions_algorithm 类型的向量，algorithm部分静态分析和改写代码目录位于 /src/esbmc/goto_functions/ 文件夹下，根据检索目前能检索到的直接继承 goto_functions_algorithm 的算法有： goto_contractor, unsound_loop_unroller, mark_decl_as_non_det, goto_cse
问题：applying goto contractors具体做了什么？
(4) goto_inline/goto_paritial_inline
(5) 如果命令行有设置gcse, 利用value_set_analysist进行Value-Set分析
问题：此处的Value-Set分析的原理以及如何改变goto_functions？
(6) goto_cse: common subexprssion elimination, 将含有多个计算符号的表达式拆成多步
(7) 如果有设置interval_analysis, 进行interval_analysis分析
问题：此处的Interval-Analysis如何反应到goto-functions上
(8) 如果有设置inductive-step, k-induction等相关cmdline args, goto_k_induction(goto_functions)
问题：为了做k_induction需要进行什么预处理？
(9) goto_check(goto_functions)
goto_check到底使用来干什么的？
a. 根据optionst从命令行参数读取并将goto_checkt内的相关数据结构进行设置：
disable_bounds_check, disable_pointer_check, disable_div_by_zero_check, disable_unlimited_scanf_check,enable_overflow_check,enable_unsign_overflow_check, enable_nan_check
b. 调用goto_check(goto_programt &goto_program)函数，该函数会便利goto_programt中的每一条指令i，首先会调用check(i.guard, i.loc), check会调用check_rec函数， 由于该处address输入为false，直接进入switch语句，根据expr也就是i.guard的类型来进行不同的处理，直观上来说check_rec会不断递归地对逻辑连接操作符向下层的表达式进行调用(此处的不断向下递归的路径可能对应其路径的约束，在函数的guard中进行记录和回溯)，而对可能产生上述问题的操作，当递归碰到相应的表达式类型的时候调用其check函数：例如在递归解析到expr2t::div_id, expr2t::modulus_id的表达式类型时，会调用div_by_zero_check(expr, guard, loc)，这类check函数会通过表达式内的元素创建违反性质的公式，如该例子中为 notequal2tc(side_2, zero)，并调用add_guarded_claim来创建该性质的claim（该函数内部即在goto_checkt的new_code数据结构的末尾加上ASSERT的instruction，其产生提田间为guard和其违反的性质，该创建的new_code也就是assertio最终在goto_check最后会被加到当前处理的instruction的前面）。
(10) remove_no_op(goto_functions)
(11) remove_unreachable(goto_functions)
此处解析判断的unreachable code具体指的是哪些？
根据注释描述，当前ESBMC作者仅仅做了对没有使用到的函数调用对应的code进行了去除
(12)多线程相关的：add_race_assertions, 等等
3. output_goto_program(options, goto_functions): 将生成和预处理过的goto输出或者翻译为C等操作- set_claims: 设置用户自定义的claims，从代码目前看来只是将claim的string atoi后的unsigned值存了下来
问题：什么样的claim是用户自定义的？用户如何自定义claim? - 创建bmct数据结构： bmct bmc(goto_functions, options, context);
bmct数据结构包含些什么信息？
bmct包含const contextt &context, namespacet ns, smt_convt指针 runtime_solver 以及 reachability_treet指针 symex，其中比较核心的是reachability tree的数据结构symexreachability_treet会记录什么信息？
（此处仅列举关键信息）- goto_functions
- 一个execution_statet的链表，其中的状态表示当前多线程interleave的执行状态，改执行对应的是程序运行时的状态序列
execution_statet数据结构包含了什么信息？
execution_statet继承了goto_symext的所有成员变量：goto_symext是来自于CBMC的符号执行状态定义，其中比较关键的成员变量有：
A. call_stackt call_stack; 符号执行的函数调用栈， call_stackt是framet的一个链表，framet中包含对函数名的描述function_identifier, goto_state_mapt goto_state_map用来记录需要被merge到一起的state(key是其需要被merge的点)， L1层级的重命名，函数调用的location, 函数的结束以及返回值，以及当前函数内的函数指针等
B. unwind_set，用来记录loop的展开次数，key为loop的id
C. symex_targett指针target; 根据监听trace的符号执行构建的符号执行结果
D. goto_symex_statet *cur_state;当前的执行状态
E. allocated_obj的list dynamic_memory， 当前动态分配的对象链表- 当前的execution_statet执行状态cur_state_it
- symex_targett schedule_target， 根据当前多线程的schedule 模式得到的bmc结果
- schedule_total_claims, schedule_remaining_claims 当前已有的claims数量和剩 余的claims数量
- next_thread_id下一个切换的进程的id
reachability tree会记录goto_functions, 当前执行的阶段性结果target，以及最终要的在进行符号执行时探索的状态集合
问题：context和ns的具体作用是什么？
除此之外bmct还负担执行符号执行，进行翻译得到smt公式以及运行判定算法的功能
- do_bmc/do_bmc_strategy: 执行BMC算法（根据是否指定BMC策略: do_bmc(bmc)
-
调用bmct中的start_bmc()方法：
该方法首先创建symex_target_equationt数据类型的指针eq，该数据类型为bmc符号执行最终产生的中间SSA表达式，该数据结构核心含有成员变量 SSA_steps, 为SSA_stept的list, 在SSA_stept中， 会记录SSA的source， SSA表达式的类型（ASSIGNMENT, ASSUME, ASSERT, OUTPUT, SKIP, RENUMBER中的一种），并且根据不同的类型，该数据结构为其预留了存储相关表达式expr2tc的成员变量
最后调用函数run(eq)，运行BMC算法，BMC算法的do-while循环的跳出条件是其存储的reachability tree是否能够setup_next_formula(), setup_next_formula()又继续会调用reset_to_unexplored_state()：
该函数依次将execution_states中的当前状态pop，将其上一步设为当前状态，也就是对符号执行状态进行回溯，如果回溯的状态能够继续进行另一种方式的interleave（对应的条件判断函数为step_next_state()），回溯时由于我们对每个状态都进行了guard的记录、会相应的修改total_claims, remaining_claims等参数。step_next_state()如何判断当前状态能够继续进行执行和搜索？
强行进行上下文切换，并触发多线程分析，分析会判断当前是否有能够继续符号执行的thread, 从而判断是否能继续进行BMC -
在上述do-while搜索不同的interleave的情况下，调用run_thread(eq)来对单个线程进行符号执行，得到smt_convt::reultt res, run_thread的具体流程为
(1) 调用get_next_formula()或者get_schedule_formula()来获得符号执行的结果
get_next_formula在还存在线程没有完成符号执行时，在没有出现上下文切换并且当前状态能够继续执行的情况下（has_cswitch_point_occured, check_if_ileaves_blocked, can_execution_continue），调用reachibility tree的当前状态cur_state的symex_step(reachability_tree)方法，此处为符号执行/BMC算法的核心：symex step首先会获取当前的reachability tree的激活的状态，并且调用goto_symext::merge_goto()函数merge_goto()的作用
merge_goto()首先读取当前状态cur_state的top frame, 并判断当前状态在source处的pc值是否为当前frame的goto_state_map的某个key，如果是则需要进行merge，否则直接return
如果进行merge：对map对应的state list中的每个待merge goto_state进行枚举，先调用merge_state_guard，将goto_state和cur_state的guard进行合并（也就是进行带化简的disjuntion连接）
随后在merge后的guard部位false的情况下，依次调用phi_function, merge_locality, merge_value_sets的操作：
- phi_function: 首先从cur_state和goto_state中把level2的命名的变量抽取到variables和goto_variables中，随后 计算一个tmp_guard，该temp_guard为goto_state的guard去除掉和cur_state的guard内的公共部分得到的guard，随后遍历cur_state中namespace的所有variables, 判断goto_state中的level2的变量是否和cur_state中的level2变量一致，如果一致则不用进行新的赋值，如果和cur_state的level2变量相比发生了变化则利用variable的base_name在namespace中找到对应的symbol，利用symbol的id和symbol的类型，创建cur_state_rhs和goto_state_rhs，并通过rename_to_record进行重命名
问题：这里的namespace的作用是什么？rename_to_record的功能是什么？换句话说命名在ESBMC中是怎样的处理机制？
最终根据两个状态的temp_guard也就是不同的部分的ifthenelse语句，对其merge后的变量赋值创建表达式 rhs = if2tc(type, tmp_guard.as_expr(), goto_state_rhs, cur_state_rhs)， 随后创建一个lhs表达式并将symbol也就是从namespace表中获取到的变量的数据结构内容的类型利用migrate_expr函数迁移到lhs这个新创建的表达式上
migrate_expr函数的作用是什么？
利用migrate_type迁移表达式的类型，并根据不同的expr的id类型，将其值也对应递归地迁移到新表达式
之后将迁移过后的新表达式new_lhs赋为lhs, 然后根据cur_state重命名new_lhs和rhs, 记下二者之间的assignment关系，并在target中创建其assignment的SSA
问题：这里为什么需要做migrate而不是之间赋值， new_lhs的必要性在哪里？
- merge_locality(goto_state): 简单地将goto_state中的local_variables合并到cur_state当前的topframe的localvaribles中，这里的local_variables的类型是l1names的集合
- merge_value_set也一样的进行集合的union
- 并且最终调节cur_state的num_instructions，这里反映的是取两个状态符号执行的相对短的一方为当前深度，从而保证我们的k部BMC对k来说是完备的
- 在对所有状态进行merge之后，将该goto_state_map中的字段进行删除因为没有merge的东西了调用merge_goto之后会根据cur_state的source.pc也就是下一步执行的指令的类型通过不同的case语句，除了几种特殊语句之外（ATOMIC_BEGIN, ATOMIC_END, END_OF_FUNCTION, RETURN），最终会执行到goto_symext::symext_step(reachability_tree)上.
问题：上述四种特殊的instruction是如何处理的？
- END_OF_FUNCTION: 首先如果是多线l1_sym程并且当前函数执行完之后会到了main函数，会将当前的线程结束，因为和main的线程合并了（TODO: 对多线程bmc原理不了解，此处暂时搁置）
- ATOMIC_BEGIN, ATOMIC_END: 对应地增加或者减少当前线程的atomic count
- RETURN: 对return的值执行symex_return: 在goto_state_list加入当前return位置的键值，可以看出对函数内的符号执行过程最终都会在return处进行merge，并且会根据当前的stack_limit进行claim声明，并通过将当前state的guard设置为false的方式，让当前状态不再进行符号执行goto_symex::symext_step(reachability_tree): 首先根据cur_state获得正在处理的instruction，随后根据instruction的类型进行不同的symex, 以下依次进行介绍
a. SKIP, LOCATION：增加pc没有其他操作
b. END_FUNCTION: symex_end_of_function():
首先会pop_frame，将当前call_stack上的framet数据结构pop出来，并将状态的guard置为刚进入function的guard因为退出function了，脱离了function内部的作用域，随后需要将结束的函数内的renaming中的local variables删除，需要在l1和l2之间将valueset和l2重命名变量删除。具体做法是根据每个local var创建指针类型的l1_sym，并且如果变量名字是alloca类型的，说明是栈上分配的内存，需要在退出函数时释放，因此调用symex_free(code_free2tc(l1_sym)),具体代码：// clear locals from L2 renaming for (auto const &it : frame.local_variables) { type2tc ptr = pointer_type2tc(pointer_type2()); expr2tc l1_sym = symbol2tc(ptr, it.base_name); frame.level1.get_ident_name(l1_sym); log_status(" clear local L1 variable:"); l1_sym.get()->dump(); // Call free on alloca'd objects if ( it.base_name.as_string().find("return_value$_alloca") != std::string::npos) symex_free(code_free2tc(l1_sym)); // Erase from level 1 propagation cur_state->value_set.erase(to_symbol2t(l1_sym).get_symbol_name()); cur_state->level2.remove(it); // Construct an l1 name on the fly - this is a temporary hack for when // the value set is storing things in a not-an-irep-idt form. expr2tc tmp_expr = symbol2tc( get_empty_type(), it.base_name, it.lev, it.l1_num, 0, it.t_num, 0); cur_state->value_set.erase(to_symbol2t(tmp_expr).get_symbol_name()); }问题：这里的symex_free()具体流程是什么？
symex_free()的代码：void goto_symext::symex_free(const expr2tc &expr) { const auto &code = static_cast<const code_expression_data &> (*expr); // Trigger 'free'-mode dereference of this pointer. Should generate various // dereference failure callbacks. expr2tc tmp = code.operand; dereference(tmp, dereferencet::FREE); // Don't rely on the output of dereference in free mode; instead fetch all // the internal dereference state for pointed at objects, and creates claims // that if pointed at, their offset is zero. internal_deref_items.clear(); tmp = code.operand; // Create temporary, dummy, dereference tmp = dereference2tc(get_uint8_type(), tmp); dereference(tmp, dereferencet::INTERNAL); // Only add assertions to check pointer offset if pointer check is enabled if (!options.get_bool_option("no-pointer-check")) { // Get all dynamic objects allocated using alloca std::vector<allocated_obj> allocad; for (auto const &item : dynamic_memory) if (item.auto_deallocd) allocad.push_back(item); for (auto const &item : internal_deref_items) { guardt g = cur_state->guard; g.add(item.guard); // Check if the offset of the object being freed is zero expr2tc offset = item.offset; expr2tc eq = equality2tc(offset, gen_ulong(0)); g.guard_expr(eq); claim(eq, "Operand of free must have zero pointer offset"); // Check if we are not freeing an dynamic object allocated using alloca for (auto const &a : allocad) { expr2tc alloc_obj = get_base_object(a.obj); while (is_if2t(alloc_obj)) { const if2t &the_if = to_if2t(alloc_obj); assert(is_symbol2t(the_if.false_value)); assert(to_symbol2t(the_if.false_value).thename == "NULL"); alloc_obj = get_base_object(the_if.true_value); } assert(is_symbol2t(alloc_obj)); const irep_idt &id_alloc_obj = to_symbol2t(alloc_obj). thename; const irep_idt &id_item_obj = to_symbol2t(item.object). thename; // Check if the object allocated with alloca is the same // as given in the free function if (id_alloc_obj == id_item_obj) { expr2tc noteq = notequal2tc(alloc_obj, item.object); g.guard_expr(noteq); claim(noteq, "dereference failure: invalid pointer freed"); } } } } // Clear the alloc bit. type2tc sym_type = array_type2tc(get_bool_type(), expr2tc(), true); expr2tc ptr_obj = pointer_object2tc(pointer_type2(), code.operand); dereference(ptr_obj, dereferencet::READ); expr2tc valid_sym = symbol2tc(sym_type, valid_ptr_arr_name); expr2tc valid_index_expr = index2tc(get_bool_type(), valid_sym, ptr_obj); expr2tc falsity = gen_false_expr(); symex_assign(code_assign2tc(valid_index_expr, falsity), true); }此处代码阅读碰到的问题：
为什么要调用两次dereference，这两次dereference用不同的mode做的事情是什么，internal_deref_item的语义是什么以及内容是如何被添加的？
第一次deference的调用是freemode，dereference会调用dereference_expr函数，dereference_expr会根据表达式的类型掉哟给你不同的dereference函数，该结构递归的函数，最终会调用dereferencet::dereference， 该函数会将dereference的指针对应的指针分析出的所有可能的指向也就是利用get_value_set来对获取可能指向的对象，并调用build_reference_to函数。
build_reference_to函数的作用?
构建指针的reference指向，根据mode构建failure的callback条件，返回一个dereference的表达式。如果是free mode，根据代码返回的表达式是个空表达式也就是free mode不关心内容，只是建立dereference的failure callback
如果是internal mode，dereference会根据build_reference_to中所有可能指向的内存对象，将其封装为结构题添加到internal_items中，并每次将其dump到goto_symex的internal_deref_items中，其中存放的结构体定义为dereference_callbackt::internal_item，其创建的代码如下internal.object = value; // Converting offset to bytes internal.offset = typecast2tc( signed_size_type2(), div2tc( final_offset->type, final_offset, gen_long(final_offset->type, 8))); internal.guard = pointer_guard; internal_items.push_back(internal);代码中 object存放的value是最后指针指向的内容的基地址，这里的value的值是将dereference的对象进行to_object_descriptor2t类型转换后得到的o.object, final_offset是对o的offset进行bit类型转换之后的bit offset，在最终转为internal的object时，此处final_offset的类型为bit类型
为什么直接进行to_object _descriptor就能够直接拿到dereference对象的相关信息，这些信息是如何维护的？为什么能够直接拿到？Offset的具体语义是什么？
该问题留到symex_assign部分进行回答
继续对symex_free进行分析：
在两次deference进行调用后，在internal_deref_items中拿到了内部的dereference object，因为是symex_free所以对被free的内存对象有offset的要求，对于internal_deref_items中的每个内存对象，创建该内存对象对应的guard g，从item中拿到对象的offset，并创建当前offset等于0的表达式eq，并添加claim，因为free的对象的offset应该为0。随后，对所有的alloca创建的内存对象也就是存在allocad里面的内存对象，会依次加入当前free的对象id_item_obj和alloca出来的对新安个 id_alloc_object不等，因为这些alloca的变量不需要进行free
问题：如果不对alloca进行free后续该部分如何判断其已经不再当前的生命周期内不能使用？
在对internal items每个可能的指向的对象进行了alloca判断和相应的assertion编码后，最后symex_free需要执行free的语义，如以下代码所示，这里sym_type表示哦创建一个array的变量类型，紧接着用输入的expr也就是code.operand创建pointerobject，并且再次调用read模式的dreference，这里的大概意思应该是让dereference自动构建出ptr_object指向的对象，随后根据得到的解引用的对象，进行allocbit的消除操作，这里首先用valid_ptr_arr_name和创建的bool类型的数组，随后用index2tc创建从该该array的index表达式，也就是valid_sym对应的array便利那个在index为ptr_obj的内容，最终生成false表达式并调用symex_assign，来处理将该false表达式赋值给valid_index_expr所表示的array表达式上，从而完成对该ptr_obj所表示的allocbit的false赋值// Clear the alloc bit. type2tc sym_type = array_type2tc(get_bool_type(), expr2tc(), true); expr2tc ptr_obj = pointer_object2tc(pointer_type2(), code.operand); dereference(ptr_obj, dereferencet::READ); expr2tc valid_sym = symbol2tc(sym_type, valid_ptr_arr_name); expr2tc valid_index_expr = index2tc(get_bool_type(), valid_sym, ptr_obj); expr2tc falsity = gen_false_expr(); symex_assign(code_assign2tc(valid_index_expr, falsity), true);这里的array的类型的index的类型是否一定为index还是是generalize的array？
c. GOTO:
case GOTO: { log_status(" ======= goto symex: GOTO"); expr2tc tmp(instruction.guard); replace_nondet(tmp); dereference(tmp, dereferencet::READ); replace_dynamic_allocation(tmp); symex_goto(tmp); }首先goto 的instruction中一般含有条件，该条件内可能会存在非确定性的操作或者sideeffect，首先会将 instruction的guard提出给tmp，然后调用replace_nondet(tmp)，该函数会判断该guard内是否是非确定性的sideeffect或者说是一个数值表达式其中包含非确定性的term，如果是前者直接创建nondeterministic的symbol来进行替换，如果是后者就递归调用去替换。
问题：这里的replace_dynamic_allocation(tmp)的具体作用是什么？为什么都要先dereference然后进行relacement，这样的操作的具体含义是什么？
symex_goto首先会将当前的instruction也就是pc提出，随后创建new_guard以及判断当前的guard是否是true或者false，并且将当前的跳转的target记为goto_target, 根据instruction的顺序，判断跳转到的pc点实在当前的state的前方还是后方，如果是前方记forward为true。如果是backward则可以将当前的跳转语义看成循环，又一次地走到当前的goto标识，说明又进行了一次循环，则需要对unwind的次数进行+1，并根据当前的跳转条件生成新的guard，并加入loop_bound超过限制的claim。之后根据forward和backward的情况，创建出下一条pc点state_pc，并且由于当前的语句是goto，我们需要将当前的状态记录下来和之后的状态进行merge，所以statet::goto_state_listt &goto_state_list = cur_state->top().goto_state_map[new_state_pc]; 并且将当前的状态push到list中，goto_state_list.emplace_back(*cur_state);
如果当前的跳转不是foward，并且如果goto跳转的位置就是当前的位置，那么当前的goto语句相当于一个assume语句，则如果当前的guard为true，则 assume(gen_false_expr());, 否则的话对当前的new_guard取not后再assume，assume()函数会对读入的assumption参数进行rename之后，调用target的assumption函数，加入target的SSA_steps中，并return. 如果goto的位置不是当前的pc，那么说明该goto语句组成一个循环结构，通过拿到instruction对应的loop_number
loop number实在什么时候指定的？
拿到该循环的unwind次数unwind，并将其增加1，如果当前的unwind次数通过调用get_unwind发现已经超过loop_max_unwind，那么通过调用loop_unbound_exceeded，将当前的new_guard加入到对应的claim中，并且将unwind重置为0，因为后续可能还会执行到这个循环，并将当前的状态cur_state的pc加一，如果当前的new_guard是true，那么该循环不会终止，因此直接return。随后我们来处理merge的相关事项，首先创建两个targett类型的pc点：new_state_pc以及state_pc, state_pc表示当前状态下一次执行的pc, new_state_pc表示，为了merge创建的新的状态的pc点，根据forward和backward的不同。
- 如果是forward，那么跳转到的点为goto_target, 因此新的状态的pc点直接置为跳转到的语句pc，当前状态state_pc继续顺序执行，因此对其进行加一操作。
- 如果是backward，那么新创建的new_state_pc应该是当前goto的pc加一，因为进行merge的点应该是跳出循环也就是goto的下一条语句，而当前状态state_pc应该跳转到goto_target进行执行。
随后我们将state_pc赋值给cur_state->source.pc, 随后将当前状态push创建的goto_state_map[new_state_pc]中，在该操作完成之后，我们需要对cur_state也就是不进行goto跳转的状态进行新的guard创建，其基本思想就是将goto的guard根据是否跳转取new_guard的非或者是直接用new_guard，对应backward和forward，这里不赘述。
d. ASSUME:
symex_assume的语义即简单的对assume中的表达式的nondet部分进行替换，并对cond调用dereference，使其中使用到内存的操作变为内存对象，最后对内存对象进行replace_dynamic_allocation。问题：同样是上面碰到的问题，为什么要dereference并且replace？e. ASSIGN：
对assign语句的处理首先要将输入的expr转换为code_assign的数据类型，并将从code当中提出target和source，分别作为lhs和rhs表达式，并且将original_lhs也设置为target. 随后对lhs，rhs中的非确定性行为进行symbolic的替换，并对lhs，rhs进行dereference操作，模式分别为WRITE和READ
问题：这里WRITE和READ的mode对dereference的结果有什么样的影响？
在dereference过后，将dynamic分配的变量替换为array的member，随后根据rhs是否存在sideeffect来执行sideeffect的assign，这里重点对sideeffect的两个种类进行分析：malloc和alloca。- malloc: symex_malloc调用symex_mem(true, lhs, code)，symex_mem中首先将alloc的类型抽取到type中欧国难，将分配的size分配到size变量，如果不是trivial的情况，用cur_state对size符号进行rename，保证其是当前状态下的符号值，如果size是常量并且为0，则分配地址为一个空指针，直接返回名字为NULL的指针类型的表达式。否则将当前的dynamic_counter进行加一操作，并创建一个symbol，将名字明明为 symex_dynamic::dynamic_(dynamic_counter_value/array根据长度是否为一),随后用namespace对当前的分配的类型type进行调用follow
问题：这里的ns.follow的作用到底是什么？
对type进行rename得到的renamedtype, 之后会将创建的symbol的type 设为dynamic, 如果分配的长度为1, 那么symbol的类型直接给为renamedtype, 否则将类型设为typet::t_array，并且subtype为renamedtype, 随后在context中加入symbol，至此我们已经创建好了内存对象symbol，随后我们还需要创建内存对象symbol的地址，同样的分size是否为1,来进行创建，这里仅描述不为一的请抗，首席那创建类型subtype，subtye是symbol的type的subtype，随后创建symbol sym表示数组，创建数组index为0的公式idx_val,然后创建数组sym在idx_val上的寻址也就是subtype类型的表达式idx, 此时将rhs_ptr_obj设为idx，表示rhs的地一个指针指向的数据对象，最后调用address_of2tc创建rhs_type类型的指针rhs_addrof,并将rhs赋为该表达式，最终复制一个rhs，首先调用symex_assign(code_assign2tc(lhs, rhs), true), 其中一份用于创建pointer_object2tc，并调用track_new_pointer(ptr_obj, new_type), track_new_pointer会做的事情：
a）. 利用symex将dynamic info array的ptr_obj的index设为true
b）. 利用symex将valid ptr array 的ptr_obj处设为true
c）. 利用symex将alloc size array 的ptr_obj处设为传入的size（当size不是nil的情况下）
另外一份emplace_back到dynamic_memory中 - alloc，和上述类似除了名字不同
在处理完了上述sideeffect之后，调用symex_assign_rec(lhs, original_lhs, rhs, expr2tc(), g, hidden_ssa), 直观上来说该函数通过判断lhs的类型，来调用不同的symexassign对象，这些symexassign对象会根据类型递归地将赋值语句最终都拆解为多条symex_assign_symbol, 因此我们这里来看symex_assign_symbol的功能：symex_assign_symbol主要用来对lhs rhs进行rename后创建target中的assign SSA_step表达式，但是在这之前会调用cur_state->assignment(renamed_lhs, rhs)，在函数中会进行常量传播、valueset的赋值
问题：常量传播是怎么做的？
问题：valueset的赋值会进行什么样的操作？
问题：valueset的赋值和dereference中的valueset有什么样的联系？(2) 对得到的symex_target_equationt结果 eq, 执行SSA_step_algorithm, 这里根据印象应该主要做的事情是根据assertion多SSA进行slicing
(3) 调用run_decision_procedure对生成的验证条件进行翻译和利用SMT求解器进行求解
-
-
