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