GCC扩展：自动检查编码规则的工具

理论计算机科学电子笔记248（2009）149-159www.elsevier.com/locate/entcs一种集成在GCCGuillemMarpons1，4JulioMarinBronco1，4ManuelCarro1，3，4A'ngelHerranz1，4Lars-RébenAkeFredlund1，2，4UniversidadPolit'ecnicadeMadridBoadilla del Monte，SpainJuanJos'eMoreno-Navo1，4UniversidadPolit'ecnicadeMadrid，IMDEASoftwareBoadilla del Monte，SpainA'lvaroPolo5Telef′onicaI+D马德里，西班牙摘要编码规则通常用于工业中，以促进软件编码时的最佳实践，并避免C或C++等语言中存在的许多危险结构。 需要可预测的、可靠的工具来自动衡量对这些实践的遵守情况，因为手动检查合规性很麻烦。 此外，由于可能的编码规则集的范围很广，因此需要易于定制为了使这些工具具有实际用途。考虑到这一目标，我们提出了一个GNU编译器集合（GCC）的扩展，它对那些不符合编码规则的代码片段进行了标记，到一个给定的集合。 这些编码规则集可以使用高级声明性语言来定义，逻辑编程，从而使得可以容易地检查代码是否符合针对项目、公司或应用领域的特定需求的关键词：编码规则检查，编程环境，质量保证，逻辑编程。1工作部分得到西班牙工业、贸易和旅游部的PROFIT赠款FIT-340005-2007-7和FIT-350400-2006-44以及马德里自治区的赠款S-0505/TIC/0407（PROMESAS）的支持。2我们得到了西班牙科学和创新部的Ram'onyC ajalgran nt的部分支持。3由西班牙科学和创新部2008-05624/TIN（DOVES）赠款和欧盟通信和技术计划（S-Cube）项目编号215483部分支持的4电子邮件：{gmarpons，jmarino，mcarro，aherranz，lfredlund，jjmoreno} @ fi.upm.es5电子邮件：apv@tid.es1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.07.065150G. Marpons等人/理论计算机科学电子笔记248（2009）1491引言像C或C++这样的语言需要以一种有纪律的方式使用，以最大限度地减少由于其弱点和更容易出错的特性而造成的危险。为此，在行业中通常要求代码只依赖于语言的一个定义良好的子集，遵循一组编码规则。一些标准规则集确实存在，列出了给定语言的良好通用编程实践，如High-Integrity C++ （ CIPPP [10] ） 。 MISRA-C [8] 是 汽 车 工 业 软 件 可 靠 性 协 会（MISRA）制定的另一项领先举措。它包含了141条旨在编写健壮C代码的编码规则关键系统。在实践中，许多组织然而，为了使编码规则具有实际用途，需要一种自动检查代码一致性的方法，不管是谁设计编码规则集或指定其使用。有许多来自供应商的商业编译器和质量保证工具，如IAR Systems [3]和Parasoft [9]，它们声称能够以检查代码是否符合ISOPP、MISRA-C或其他标准的子集。其他工具，例如Klocwork [4]，定义了自己的非正式描述规则列表，旨在避免危险，用户可以通过复杂的应用程序接口（通常在C或C++中）添加新规则。 但是，由于缺乏正式的 和规则的简洁定义，很难确定这些工具实际上在检查什么，两个不同的工具很可能在某些特定代码的有效性方面存在分歧，例如，同样的MISRA-C规则。在[7]中，我们提出了一个框架来精确地指定规则集并自动检查（非平凡）软件项目的一致性。在规则编写器方面，基于逻辑的语言（目前是Prolog的一个子集，具有较小的语法扩展）允许轻松捕获编码规则的含义，构成了比大多数其他工具提供的更实用的用户定义规则机制。最近出现了其他提供高级语言来定义代码检查的工具，例如Klocwork Insight，Parasoft RuleWizard或Semmle Code [1]。与这些其他工具相比，我们的建议依赖于一般的逻辑编程（在Semmle代码中，所有代码查询都被转换为数据库）。借助全逻辑编程的表现力，我们可以处理在推理C++模板和模板实例属性时出现的潜在无限集合。 它还为我们提供了在结构化术语上使用统一的机会，例如，使用逻辑变量作为模板参数，大大简化了模板上规则的定义（参见[7]）。 这是以危及终止某些规则的执行，除非在规则定义语言上建立了适当的约束。我们的编码规则检查工具的另一个突出特点是，它已经集成到GNU编译器集合（GCC，gcc.gnu.org）开发工具链中。在这项工作中，我们提出了一个新版本的编码规则检查器，改进了[7]中提出的一个，提取了所有需要的信息6尽管有些规则可能是不可判定的，最终需要人为干预。G. Marpons等人/理论计算机科学电子笔记248（2009）149151规则说明（英文）规则形式化在我们的DSL编码规则编译器编译成Prolog的C++项目源文件Modifiedg++（项目构建）Prolog中的项目事实检查规则（Prolog引擎）报告列表规则违反图1. 整个规则检查过程。图的左侧部分包含相关步骤规则的形式化。在右边，描绘了程序特征提取。规则一致性检查显示在底部。在使用GCC编译C++程序时，将规则检查器和GCC工具链放在一起的一个原因是，这是一项不平凡的任务，使检查器在成千上万的开发人员的日常工具中随时可用，这无疑将促进许多项目中编码规则的采用。 此外，委员会认为，通过使用单个解析器和语义分析引擎（用于目标代码生成）来进行编译并为代码检查器收集信息，避免了关于如何解释代码的任何可能的差异（如果使用不同的解析器/分析器，则可能发生这种差异）。此外，GCC中已经存在的静态分析所收集的信息可以被重用，以实现需要它的规则2 编码规则检查我们检查某个软件是否符合给定编码规则的过程包括三个主要步骤，如图1所示：(i) 将规则7形式化为基于逻辑的领域特定语言，并自动转换为Prolog。标准规则集通常使用简单的英语进行定义。(ii) 将必要的程序信息转录到相同的表示中，Prolog事实。要分析的程序是用我们修改过的GCC版本编译的，增加了一个将这些事实转储到文件中的fipa编码规则7、事实上，它的破坏。152G. Marpons等人/理论计算机科学电子笔记248（2009）149(iii) 分析违反规则的谓词以及在适当的抽象层描述程序在我们的例子中，这是通过使用标准Prolog系统- Ciao Prolog [ 2 ]来寻找规则的反例来完成的。Prolog检查器是一个名为checkrules 8的命令行工具，它接收GCC生成的事实文件和（预编译的）编码规则本身作为输入。当前的规则定义语言是Prolog的一个子集，带有一些语法扩展（第3节）。在未来，我们计划用一种完全声明性的逻辑语言来促进规则的形式化定义，这种语言具有排序、构造性否定和适当的量化器（一些细节在[7]中给出）。我们的目标是使不熟悉Prolog的开发人员能够形式化编码规则。关于规则形式化的更多细节可以在第3节中找到，程序特征提取在第4节中讨论。3 Prolog中的结构化编码规则定义我们首先关注的是我们所说的结构化编码规则：那些必须 处理代码中的对象（如类或函数）、它们的静态属性以及它们之间的静态关系（如继承、包含或使用）。这类规则的一个很好的例子是规则3.2.4（见图2），一个抽象类应该没有公共构造函数。抽象类是那些至少有一个未实现的成员函数的类。这个规则有助于明确抽象类不能被实例化，而需要通过子类使用的事实。规则的形式化需要一组特定于语言的谓词来表示结构信息，例如，检查程序的继承图。表1显示了一些用于定义一些规则的谓词，C++语言，包括上面的例子。这些谓词构成了编写规则的编程接口，并在编译器生成的信息之上定义，如第4节所述。例如，一元谓词抽象类用于定义上述规则。规则3.2.4的Prolog形式化编码了对规则的违反，即，一个抽象类Class有一个成员Ctor，它是一个公共构造函数。如果可以违反规则，则检查规则将分析的软件中的Ctor和Class的具体实例返回给用户，并通过操作符#与规则相关联的警告消息。谓词的参数可以作为用户消息的一部分显示结构规则的另一个例子是RIPP 3.3.13，它写着它背后的基本原理是同一对象的成员函数总是静态绑定的如果从构造函数或析构函数调用。在这种情况下，返回属于同一个类的两个方法作为违反规则的见证注意使用8我们的扩展GCC和检查规则工具都可以在GlobalGCC项目的网站上找到www.ggcc.info/? q=download，GPL许可。我们试图保持我们的GCC与GCC主干同步。G. Marpons等人/理论计算机科学电子笔记248（2009）149153表1C++代码中描述结构关系所必需的谓词的子集预测平均值类和方法抽象类（c）类c有一些未实现的成员函数。constructor（m）成员m是一个构造函数。有一个类似的谓词析构函数。publicmember（m）成员函数m具有公共可见性。 有受保护和私有可见性的类似谓词。virtual member（m）成员函数m是virtual（调用方法是动态调度的）。继承（a，b）类b直接继承自a。（a，b）的传递闭包和自反闭包/ 2的直接基数。（a，b）类b的public基直接从类a继承，可访问性。对于其他可访问性选择和虚继承，也有类似的谓词：virtual base of。（成员）职能calls（a，b）（Member）函数a在其文本中有对（member）函数b的调用。overrides（a，b）成员函数a在派生类中定义为a重新声明成员函数b（它们具有相同的签名，但实现不同）。重载成员（a，b）成员函数a和b声明在同一个类并具有相同的名称（但签名不同）。声明成员（c，m）成员函数m被声明（或用新的实现）。hasmember（c，m）类c定义了一个成员函数m。 m可以是从基类继承。具有相同的sig（a，b）函数a和b具有相同的元和参数类型154G. Marpons等人/理论计算机科学电子笔记248（2009）1491HICP P 3.2。4# 数量' 这是我的错。 '：-abstract_class（Class），has_member（Class，Ctor），constructor（Ctor），public_member（Ctor）.'PadrPP3.3.13#’数量在同 一 个 班 级里 '：-hases_member（SomeClass，Caller），（构造函数（调用者）;析构函数（调用者））的情况下，has_member（SomeClass，Callee）， virtual_member（呼叫者），calls+（Caller，Callee）。'PadrPP 3.3.15# 数量“a n d”#C 数量'，和d ' #C 数量' 难道你不使用虚拟吗？#’ 数量“ 的。 '：-immediate_base_of（A ，B ） ， immediate_base_of（ A ， B ） ，C ） ，B@C，base_of（B，D），（C，D）的基，\+virtual_base_of（ A，C）.1HICP P 3.3。5#’功能'#方法#'是重写通过'#覆盖#’数量’数量’数量“ 的。 '：-has_member（Derived，Overriding），overrides（Overriding，Method），overriding_members（Overloads，Method），（has_member（Derived，Overriding2），overrides（Overriding2，Overloads））.覆盖（M1，M2 ）：-declares_member（Derived，M1），immediate_base_of（Base，Derived），has_member（Base，M2），have_same_sig（M1，M2）.图2.PROLOG形式化的一些规则的PROLOG规则集中。析取（;）和特殊语法谓词+来表示传递闭包的谓词。我们对调用者直接或间接调用的方法感兴趣，因此我们使用表1中定义的谓词调用的传递闭包。规则第3.3.15条举例说明否定的用法。它说：借助伴随规则的正当性，我们可以将其重新表述如下：如果存在A、B、C和D类，则违反了规则3.3.15：G. Marpons等人/理论计算机科学电子笔记248（2009）149155\D的基类通过两条不同的路径，其中一条路径的类B为 A的直接子类，另一个具有C类作为直接子类其中B和C是不同的类。而且A不是C的虚基。该规则是用Prolog编写的，如图2所示。 阴性失效（操作） ator+）出现在最后一行。 由于最后一个Prolog目标的语义依赖于在逻辑变量A和C的实例化状态上，子句内的目标的顺序变得相关，不仅是为了性能考虑。为了避免这种情况，我们计划用建设性的、逻辑上有意义的否定来取代否定即失败。特别是，我们正在研究建设性内涵否定的适用性[5]。在这个例子中，我们还使用操作符@来获得不同的类对，其中B和C不能互换它们的角色。最后，规则RIPPP 3.3.5举例说明了否定的一个更复杂的用法：必须“覆盖基类虚函数的所有重载。“显示规则的代码在图2中，连同使用的谓词之一的Prolog实现，定义它：两个类方法之间的重写关系4使用GCC收集程序信息GCC的中间端包含一组转换和优化过程 它独立于编译语言和目标体系结构。编写规则所需的许多（但不是全部）程序特性都是通用的到多种语言，并在中端有一个共同的表示，甚至如果语义在不同的语言之间可能不同。例如，作为模板和朋友的构造几乎是C++独有的，只有C++前端知道它们。在我们的GCC扩展版本中，我们对中端和C++前端都进行了检测（总共大约2.8KLocs的新代码），但大部分分析都是在新的中端通道中完成的。在中间端实现功能有很多优点：添加新的传递简单而干净，并且没有开销，除非使用相应的标记启用传递。此外，新的功能可以重用于其他GCC语言。我们修改后的GCC将描述所分析软件（可以是程序或库）的结构属性的Prolog事实写入文件。项目中的所有源文件都必须进行分析，因为结构规则通常涉及项目范围的属性。全局分析是依靠项目中使用的建筑过程进行make、cmake、ant等）并将不同编译单元的所有Prolog事实累积在单个文件中，随后使用检查规则进行分析。对于代码中的每个相关实体，Prolog项 的 的 形式 生成实体（GLOBALKEY），其中实体是枚举、枚举值、联合、记录（结构或类）、函数、全局var、方法、字段和位字段之一。GLOBAL KEY是一个项目范围的实体标识符，基于名称mangling [11]。Mangled名称是函数名、变量名等的特殊编码。由编译器为链接器和其他具有156G. Marpons等人/理论计算机科学电子笔记248（2009）149表2表示C++全局实体之间的属性和关系的Prolog术语的结构ACCESS SPECIFIER是public、protected或private之一。virtual（method（GLOBAL KEY））accessibility（method（GLOBAL KEY），ACCESS SPECIFIER）contains（namespace（GLOBAL KEY），entity）contains（record（GLOBAL KEY），entity）enumerates（enum（GLOBAL KEY 1），enum value（GLOBAL KEY 2））extends（record（GLOBAL KEY 1），record（GLOBALKEY 2））virtual（extends（record（GLOBALKEY 2）以处理来自不同编译单元的信息。在其他可能的名称冲突中，它们解决重载的函数名，包括由模板引起的重载。局部实体的命名方案（局部变量、函数参数等）是基于其定义的范围（即全球实体）及其本地标识符。对于匿名实体（例如，匿名联合字段）生成数字标识符。按照这个识别方案，Prolog谓词存在于全局和局部实体的每个相关属性中，并且在输出中为每个属性的出现生成术语。这些术语的结构如表2所示，例如全局实体的虚拟和可访问性属性。除了个别属性之外，还存在全局实体之间的关系。 在表2中可以找到全局实体之间二元关系的一些例子：contains、enumerates和extends。像extends这样的关系也可以附加属性，例如虚拟的生成Prolog术语来表示类型并将类型附加到实体，并且还将代码位置与用户输出所需的实体相关联表1中的高级抽象谓词是使用本节前面介绍的低级谓词定义的。这种高级谓词遵循通常的C++术语（基类、成员函数等），方便了C++专家的编码规则的形式化。这种双层谓词架构还旨在更好地支持将规则检查工具扩展到其他目标语言。 关于我们修改后的GCC编译器的实现的更多细节可以 在[6]中找到。5实验结果我们的工具链能够处理任意C++代码。 结合任何类似make的软件构建工具，它可以用来捕捉现有C++项目中违反结构化编码规则的行为。到目前为止，我们已经实现了12条来自于RIPP规则集的结构规则，包括本文中提到的那些，并检查了一些中小型自由软件项目是否符合G. Marpons等人/理论计算机科学电子笔记248（2009）149157表3在我们的实验中使用的C++项目，与他们的C++行的数量的措施产品展示韦尔西翁D描述KLOCBacula2.2.8基于网络的备份程序。19IT++3.10.12信号和语音处理库。46PPL 0.9帕尔马多面体库：数值ab-60分析复杂系统的方法。dlib 17.0库 约 threading，networking，77数据压缩等等。表4规则检查过程中不同步骤所消耗的违反规则的次数和用户时间（秒） BT是项目的总建造时间，BTCR是具有结构的总建造时间数据收集已启用。LT是检查规则加载项目所花费的时间。标有规则编号的列在每个单元格中显示违规次数（上图）和检查时间（下图）。P2PP规则（编号 违反行为，检查时间）产品展示BTBTCRLtBacula76.178.968.5IT++307.4338.7300.4PPL296.3477.2235.5dlib8.610.741.33.2.43.3.13.3.23.3.53.3.63.3.70010000.010.000.000.000.000.001001684113234.400.000.1244.4325.089.2102053413301.910.000.0953.932.640.078717404060.980.000.1334.6917.320.80P2PP规则（编号 违反行为，检查时间）项目3.3.83.3.133.3.143.3.153.4.53.4.6000060Bacula0.000.010.010.000.000.00723200827IT++116.957.480.250.020.190.0975000560PPL97.380.970.080.000.080.0422420014229dlib49.150.950.040.020.190.05他们表3简要描述了分析的项目。表4报告了在每个项目中发现的违反规则的数量，以及有助于评估我们方法可行158G. Marpons等人/理论计算机科学电子笔记248（2009）149性的时间消耗信息G. Marpons等人/理论计算机科学电子笔记248（2009）149159真正的项目。 实验已在Intel Mobile Core 2 Duo 1.20上运行GHz，2 Gb RAM，项目采用-O2优化封装。当启用-fipa-codingrules在编译期间提取结构信息时，构建时间会增加。在以下情况下，时间惩罚小于5%：Bacula，但超过60%的PPL。一般来说，当模板被广泛使用时，速度会变慢。尽管dlib很大，但报告的构建时间很短，因为构建过程很简单，只生成一个对象文件。一般来说，checkrules加载一个项目的数据需要相当长的时间（在大多数情况下，与完整构建的数量级相同，但dlib由于上述原因除外）。这是因为GCC没有C++全局编译的概念，并且头文件在项目构建期间被编译多次，产生了大量冗余信息。另一方面，检查时间从几分之一秒（即， 0.00时间）到超过1分钟。从经验上讲，复杂的子目标被否定的规则是那些需要更长时间的规则。事实上，由于对规则的计算复杂度没有限制，因此执行时间可能是无限的。尽管如此，观察到的性能对于一个项目范围的静态分析工具来说是合理的，这个工具并不意味着在每次编译中都运行请注意，尽管我们发现了许多规则的大量违规行为，但在这些项目中，没有违反3.3.14和3.3.15。 一个原因是它们处理程序员很少使用的语言特性（分别是抽象类中赋值运算符的声明和重复继承6结论和今后的工作我们已经提出了一个用于结构化编码规则验证的工具，其中C++的规则通过声明性规则定义语言进行形式化定义。用户可以定义自己的规则，该工具无缝集成到开发人员的工作流程中。有关程序的基本信息来自用于生成目标代码的同一编译器（GCC），这避免了不一致性。只有大约20%的规则是纯结构性的。实现更多的规则需要修改编译器的其他部分，并获得GCC中端不可用的语法信息以及GCC在其优化步骤中执行的复杂分析的结果。我们计划扩展我们的规则定义语言，以支持新的逻辑形式主义，帮助定义非结构化规则。这种方法应该很容易适应GCC支持的其他语言，这将需要其他前端的仪器引用[1] de Moor，O.，D. Sereni，M.Verbaere，E.Hajiyev，P.Avgustinov，T.Ekman，N.Ongkingco和J.提布尔，.ql：使面向对象的查询变得容易，在：R. Lüammel，J. Visser和J. Sarai va，editors，GTTSE，LectureNotes in Computer Science5235（2007），pp. 78-133.160G. Marpons等人/理论计算机科学电子笔记248（2009）149[2] Hermenegildo，M.，F. Alberto，D. Ca beza，M. Carro，M. Gar c'ıadelaBanda，P. L'opez-Garc'ıa和G.普埃布拉，CIAO多方言编译器和系统：未来（C）LP系统的实验编译器，在：逻辑和约束逻辑编程的并行性和实现，新星科学，Commack，纽约，美国，1999页。65比85[3] IAR Systems，http://www.iar.com/。[4] Klocwork，http://www.klocwork.com/。[5] Mari nBagio，J.， J. J. Moreno-N avarro和S. M. Hernáandez，Implementingconstructiveintensional negatio n，New Generation Computing 27（2008）.[6] 马邦斯，G.， J. MarinBagio和A' 。 Polo，A. D.C.D.C. J. Hutton，C. C.罗斯和J. W. Lockhart，editors，Proceedings of the GCC Developers43比54[7] 马邦斯，G.， J. Marinobelo-Carballo，M. Carro，A'. Herranz-Nie va，J. J. Moreno-N avarro和L.- A. 应用逻辑程序设计进行自动编码规则一致性检查，在：P。哈达克和D. S. Warren，编辑，声明性语言的实用方面，计算机科学第4902（2008）号来文，第4902（2008）页。18比34[8] MIRA有限公司， C语言在关键系统中的使用指南（Guidelines for the Use of the C Language[9] Parasoft，http://www.parasoft.com/。[10] 编程研究小组，[11] 维基百科，http://en.wikipedia.org/wiki/Name_mangling网站。