自动推理如何提升视频体验
自动推理是机器进行逻辑推理的能力。自动推理的一个常见应用是软件验证，即确认计算机程序将按预期执行。尽管这已成为活跃研究领域五十年之久，但直到最近验证技术才适用于具有数百万行代码的工业代码库。
自2019年以来，某中心视频自动推理团队一直在创建软件开发工具，利用这些验证技术为开发人员提供对其编写代码的更大信心。该应用程序控制所有视频内容的播放。
视频应用程序提供统一的终端用户体验，无论内容类型如何，从点播电影到大型体育赛事的直播流媒体。由于该应用程序具有由全球数十个独立团队使用多种编程语言开发的多个组件，并且必须在数千种不同的硬件配置上运行，这为自动推理提供了一个特别艰难的环境。
自2021年3月26日起，所有视频开发人员都在使用名为BugBear的自动推理机器人，该机器人进行自动代码审查，在检测到潜在问题时提供清晰且可操作的评论，或者确认未发现问题。BugBear具有针对C/C++、Java和TypeScript的分析器，这些是视频中使用的主要语言。
BugBear实战示例
在2020年下半年开始的试点活动中，BugBear进行了1,000多次自动代码审查，并在其中约100次中识别出潜在问题。视频开发人员同意其中约80%的问题需要代码修改。
BugBear完全使用某中心云服务实现，并在15分钟内提供对开发人员代码的反馈。它可以识别通用问题和违反视频特定业务逻辑属性的情况，我们称之为代码契约。
通用问题是代码中始终被认为是错误的问题，无论应用程序应该做什么 - 例如，打开文件后未关闭它，或尝试使用先前未初始化的变量值。
代码契约通常是对代码可能行为的限制或需要实现的特定业务规则；考虑诸如"在启用触摸屏键盘之前，检查设备是否支持触摸屏作为输入机制"之类的规则。
静态分析工具
BugBear的分析器是静态分析工具，这意味着它们不需要执行代码来发现问题。对于C/C++和Java源代码，我们采用名为Infer的现有工具，为视频进行了调整，以检测通用问题，如内存和并发问题 - 当多个进程在共享变量上并行操作时出现的问题。
强制执行契约
对于C++和TypeScript契约，我们开发了自己的工具，将分析中的程序编码为逻辑事实数据库。使用自定义规则集，它可以自动推断程序的属性。我们使用声明性编程语言Datalog来表示事实和规则。
例如，假设契约要求在函数F中，函数open_resource应始终在函数use_resource()之前调用。在Datalog中，相应的规则可能如下所示：
violation(F) :- function(F),calls(F, use_resource),not called_before(open_resource, use_resource, F).
这里的关键问题是构建called_before关系，该关系对所谓调用图的形状施加约束，调用图是通过程序指令集的可能调用序列的图形表示。
调用图的构造是一个不可判定问题，这意味着不可能构建一个完全准确、有限的图来正确编码程序中的所有函数调用。因此，我们只能在调用图的近似值上评估我们的规则。这些近似的精度和性能一直是我们研究交付BugBear的主要主题之一。
在正在进行的工作中，我们正在构建一个系统，使用户能够在代码审查中按需证明断言。例如，用户将能够在其代码中编写"BugBear断言"，这些断言将由我们的工具自动分析。这些断言也将用于扩展分析，因为我们将能够仅关注与证明断言相关的代码。
更多精彩内容 请关注我的个人公众号 公众号（办公AI智能小助手）或者 我的个人博客 https://blog.qife122.com/
对网络安全、黑客技术感兴趣的朋友可以关注我的安全公众号（网络安全技术点滴分享）
公众号二维码
公众号二维码
