x86-sat:使用Z3的x86指令的基本SAT模型，可从英特尔文档自动生成

x86卫星 这是通过解释Intel的指令伪代码，将其转换为的模型来构建x86内在函数的自动生成的形式化正式模型的初步尝试。 描述 提供了一个交互式指南，其中包含每条x86内在指令的数据，包括指定该指令行为的伪代码。内在性指南由一个XML文件作为后盾，其中所有这些数据都采用易于解析的格式，我们在这里使用它来构建Z3模型。 到目前为止，仅支持英特尔伪代码的以下功能： 基本一元/二进制算术/按位运算和三进制条件 读取和写入的位片 IF / CASE条件（在无法静态解析时以其为前提） FOR循环 函数定义/调用有关最新信息，请参阅parse.py中的tokens / rules 。 英特尔文档中使用的许多功能未在XML中明确给出。目前，几乎所有功能都不支持（有关当前列表，请参见intr_builtins.py定义的功能）。 这种生成模型的方法具有固有的局限性。内部函数仅覆盖x86指令的子集（大概