lart

LART：LLVM抽象和改进工具

LART = LLVM抽象和改进工具。该工具的目的是提供实施各种程序摘要的LLVM至llVM转换。就指令集而言，结果程序是正常的，可以执行和分析的混凝土LLVM程序。有关使用特殊LLVM固有功能和LLVM元数据节点插入（片段）程序上有效的抽象（S）的额外信息。 LART既提供了一个独立的工具，该工具可以处理盘式比特码文件，也提供了可以集成到复杂基于LLVM的工具中的框架。 LART背后的主要动机是为基于LLVM的模型检查器和其他分析工具提供“预处理器”，从而通过减少问题大小来简化其工作，而不会损害分析的健全性。 LART实施的抽象通常可以根据有关抽象的“部分”太粗糙的特定说明来完善（太粗糙的抽象会产生可见的虚假错误，可在后续分析中可见，但在原始程序中不存在）。

LLVM比特码的抽象

整个练习的目的是从LLVM比特码中抽象信息，从而使后续分析更有效（以某种精度为代价）。为此，我们主要需要能够在LLVM程序中编码非确定性选择，这可以通过专用功能（类似于LLVM Interinsics）来完成。该函数命名为@lart.choice ，将一对界限作为参数，而非确定性返回属于这些界限之间的值。

LLVM语义的扩展需要由下游工具识别。这也是唯一与标准LLVM比特码的关键偏差。许多分析工具已经在内部甚至具有外部接口实现了类似的机制。适应工具不支持@lart.choice与LART合作通常非常简单。

LART提供了其他特殊用途的功能，即@lart.meta.*家庭，但是就这些说明而言，大多数工具将能够安全地忽略其存在，就像现有@llvm.dbg.*一样。如果召集LART来提炼抽象（LART提供的每个抽象都带有相应的改进程序，则计划转换将保留这些调用，以进行相应的改进程序，通常需要查找@lart.meta呼叫，该呼叫由抽象插入）。

虽然大多数传统的抽象引擎是口译员的工作，但也可以将抽象“汇编”到程序中。可以编译符号指令，而不是（重新）解释指令。在谓词抽象的情况下，所得的比特码将直接操纵和使用估计值代替具体变量。如上所述，重要的区别在于，由于某些谓词可能具有不确定的估值（既是真实和错误），因此比特码需要做出非确定性选择。某些变量甚至可以完全抽象，所有这些变量的测试都将产生是和否答案。

建造

暂时使用或重复./devcontainer/Dockerfile的设置。

然后使用：

 ./scripts/build.sh

运行编译器

 ./build/bin/lartcc <domain> <compiler arguments> in.c

选择

 opt -load build/lib/cc/liblart_module.so -lart < in.bc > out.bc

测试

 lit -v build/test

注意： build/lartcc/lartcc必须具有exacutabple许可。