Skip to content

2022 年春季学期清华大学《软件分析与验证》课程实验平台

License

Notifications You must be signed in to change notification settings

thufv/CMinor-Verifier

Repository files navigation

简介

本项目为 2022 年春季学期清华大学《软件分析与验证》课程实验平台,作业平台提供了一个 CMinor 的验证框架,你需要在其中实现核心的验证算法。CMinor 是一个面向验证的教学语言,其包括源程序和验证标注两部分,其中源程序部分大致是 C 语言的子集,验证标注部分大致是 ACSL (ANSI/ISO C Specification Language) 的子集。从 C 语言的角度来看,验证标注是写在注释中的,不会影响 C 代码通常的编译和运行。

在本实验中你需要实现本工具中的核心验证算法部分,具体的说明请见任务说明文档

本项目使用 git submodules 来集成公开测例仓库,在 clone 后可以使用 git submodule update --remote 来更新测例仓库。

安装

本项目依赖于 .NET 6,你可以从这里下载其最新的 SDK。

你可以使用任意你喜欢的 IDE,我们推荐:

注意:建议不要通过 homebrewapt 直接安装,因为其软件源中的 dotnet 的版本很有可能是过时的。建议从这里下载最新版。

注意:如果你遇到了错误 Unhandled exception. System.DllNotFoundException: Unable to load shared library 'libz3' or one of its dependencies.,那么你需要从这里单独安装 Z3 4.8.16。

使用

为了使用在线评测功能,你需要先 fork 本仓库。

本项目基本的运行方法是在根目录下运行以下指令:

dotnet run -- --source <path>

你可以使用 --printCFG 来打印出得到的 CFG。

所支持的各命令行选项的具体含义为:

--source      Required. The source file of CMinor language (recommended with filename extension '.c').

--printCFG    The file (or 'console') to which the control flow graph is printed.

--help        Display this help screen.

--version     Display version information.

评测方式

我们不再使用传统的 OJ 来提交代码,而是用 GitHub Actions 将自动化测试直接集成进项目中。 简而言之,你的每一次 push 都相当于自动提交了代码,会触发一个名为 Build and Test 的 job,其会构建项目并评测所有测例,其得分(百分制)为:

Error when building and testing

注1:请在 fork 后将上面的 URL 中的 thufv 替换为你的用户名。

注2:以上显示的得分需要等待每次 push 所触发的 GitHub Action 执行完毕后才会被更新。

结构

该编译器的设计可以分为三个部分:

  • 前端(frontend):使用由 ANTLR 自动生成的 parser 将源文件解析为 CST (concrete syntax tree,具体语法树),再遍历 CST,生成 CFG(control flow graph,控制流图);
  • 中间表示(ir):面向验证来设计的控制流图;
  • 后端(backend):使用 deductive verification 的方法从 CFG 中生成验证条件(verification condition),再将其喂给 SMT Solver 来求解。
    • 这部分是你需要来实现的。

你唯一被允许修改、并且你也必须要修改的文件是 Verifier.cs,你需要在其中实现演绎验证的算法主体。

API 文档

如需阅读 API 文档,你可以使用 doxygen,在本项目根目录下运行 doxygen 即可生成。

所生成的 API 文档在 ./api-doc/,打开 ./api-doc/index.html 即可浏览。

贡献者

参考

CMinor 语言大致是以下语言标准的子集:

About

2022 年春季学期清华大学《软件分析与验证》课程实验平台

Topics

Resources

License

Stars

Watchers

Forks