理解Herbrand Equivalence

笔者最近在看GVN的一系列论文,总会看到一个概念叫Herbran Equivalence,依靠这种定义,能够判断一个GVN算法是否是complete的,也即检测一个算法是否是precise的,只有找到所有Herbrand Equivalence关系的算法才能称得上是完全的。

目录

  • 理解:程序表达式之间的等值关系是不可判定的
  • phi结点和普通表达式之间的相等性
  • 《一种高效的完全值编号算法》定义的值编号
    • 定义Herbrand等值关系
    • 定义值编号
  • 算法执行

理解:程序表达式之间的等值关系是不可判定的

由于检测程序表达式间一般的等值关系是不可判定的,大部分 GVN 算法都将问题做了简化,通常假设条件语句的结果在编译期间是不确定的,并且对所有的运算符都不考虑其特殊语义,即忽略它们可能满足的特殊运算法则,将不同结构的表达式看作不同的表达式. 满足这些限制条件的表达式间的等值关系被称作 Herbrand 等值关系.能够检测到程序中全部 Herbrand 等值关系的 GVN 算法被称为完全 GVN 算法.
以上内容摘自《一种高效的完全值编号算法》。
两个程序表达式是否是等值的,这个问题在编译是无法判定,例如表达式a + b 和 a * b,表面看起来二者不是相等的,但是当运行时赋值a = 2, b = 2,此时两个表达式就是相等的。假定条件表达式在编译期不确定,前提是条件表达式的值不能通过静态分析得到,也即phi结点的两个分支执行哪个是不确定的。所有的运算符不考虑特殊语义,结合下文是说不考虑两个不同运算结构之间的等价性。

phi结点和普通表达式之间的相等性

这篇论文中还举了一些算法之所以是不完全的例子——也即他们无法发现phi结点和普通表达式之间的相等性。
以下几个例子实现了论文中的几个例子。
在这里插入图片描述

例子1:在input例子中发现两个表达式x和y的相等性,在LLVM 中可以识别到此两个表达式之间的相似性并删除之。贴一个Compiler Explorer的链接。

#include <stdio.h>int input(int a, int b) {int c, d, e, x, y, z;scanf("%d", &d);if(d) {x = a + 1;c = a;} else {x = b + 1;c = b;}y = c + 1;scanf("%d", &e);if(e) {return x;} else {return y;}
}int main()
{int a, b;scanf("%d %d", &a, &b);input(a, b);
}

生成的IR主要部分如下:

  %0 = load i32, ptr %d, align 4%tobool.not = icmp eq i32 %0, 0%b.a = select i1 %tobool.not, i32 %b, i32 %a%retval.0 = add nsw i32 %b.a, 1ret i32 %retval.0

突然发现,论文给出了例子2是有问题的。
在这里插入图片描述
这里使用的标记方法是先将 ϕ \phi ϕ结点的所有分支标记完再标记 ϕ \phi ϕ结点,这本身并没有问题,问题在于 n 4 n_4 n4中的表达式应该为 x 1 = x 2 + 1 x_1 = x_2 + 1 x1=x2+1
在修改之后的情况下,当 n 4 n_4 n4基本块的结尾到 n 5 n_5 n5基本块或是 n 4 n_4 n4基本块的结尾到 n 3 n_3 n3基本块的开始都是满足 x 1 = y 2 x_1=y_2 x1=y2的情况的,但是在 n 3 n_3 n3 n 4 n_4 n4结尾这部分是不满足上述等值关系的。因此此种情况可以将两者标记为等值表达式但需要注意范围,不能贸然消除。
例子2对应的Compiler Explorer链接。
例子2:

#include <stdio.h>
int z;
int input(int x, int e, int f) {int y;y = x + 1;do {// if (x == y) {//     z = 1;// } else {//     z = 0;// }x++;// if (x == y) {//     z = 1;// } else {//     z = 0;// }if (e++ > 0) {break;} else {y++;}} while (1);return 0;
}int main() {int x, e, f;scanf("%d %d %d", &x, &e, &f);return input(x, e, f);
}

为了尽量凸显对该GVN能否正确识别,我修改了原文的例子以更好的阐述笔者的思想,读者可以自己尝试,当第一处注释打开时,编译器会判定两个表达式不相等,因此将全局变量z设置为0,第二处注释打开时,编译器会判定两个表达式相等,将全局变量设置为1.对应上图中x1和y1不相等,但x1和y2相等。

第三个例子不能用LLVM实现,因为LLVM不存在两个phi结点的依赖关系。也即图中 a 1 a_1 a1 b 1 b_1 b1之间存在着矛盾关系。
根据论文后续的描述也说明了上述例子在SSA中不成立。相关描述如下:

本文中的模型和算法都基于静态单赋值形式的程序. 在一个静态单赋值形式的程序中,所有变量都有唯一的定值语句,并且所有对变量的使用都被该变量的定值语句所支配,即从程序的入口到达对该变量的使用的所有执行路径都一定经过该变量的定值语句.

可以看到,在上述例子中b1的第一次使用并没有经过其定值。

《一种高效的完全值编号算法》定义的值编号

论文的第二和第三部分分别给出了Herbrand等值关系和值编号的定义。

定义Herbrand等值关系

首先来看第二部分。
在这里插入图片描述
此公式首先定义了某个值到一个表达式的定义,作者的思路是将所有的值都上溯到定义他们的表达式的形式,这样可以比较不同值之间的相等性,带着这样的想法再来看上述公式,第一种情况是t=x的形式(根据后文的描述称为变量表达式),直接将x的表达式传递给t,第二种是t = t1 o t2的二元表达式形式(根据后文的描述称为包含运算符的表达式),将两个二元表达式的操作数的定义进行二元计算。
在这里插入图片描述
其后作者又定义了一个转换函数,也即经过一个程序节点(语句)之后表达式集合的变化,第一种可能是赋值语句,直接将表达式中的t换成x。如果是phi结点,将每条分支上的都进行转换。
在这里插入图片描述
有了单个节点的处理方式,就能够得到一条路径的处理方式,无外乎将不同节点之间的转换函数连接,当遇到phi节点时,当路径明确的情况下也就能选择出某个分支。
在这里插入图片描述
基于上述公式给出了一个P-Herbrand关系,这里的P是Partial的简写,突出了当前路径只是一种可能的运行情况。这个公式定义的不清晰,根据下文的描述应该是检测了某个路径下的Herbrand等值关系。
最后一句话是说当P是所有路径的集合时,得到的Herbrand等值关系不再是部分的,所以可以省略前缀P-。

定义值编号

值编号定义前,作者先定义了两个值编号之间的比较,有如下公式。
在这里插入图片描述
集合原文的描述更容易理解,这里我只说一个问题,第三行两个表达式写反了,应该是第二行最后一部分的否定,否则第二行和第三行不能构成一个分支上的完备集。
在这里插入图片描述
上述定义很明显,如果有变量表达式,那么从其等值集合中取一个最小的表达式作为当前变量的值编号,如果一个表达式是运算符表达式,取最小两个表达式的运算结果作为值编号。

算法执行

这一部分可以结合原文的例子来看,更好理解。

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.mzph.cn/news/611316.shtml

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈email:809451989@qq.com,一经查实,立即删除!

相关文章

2024.1.10

完善对话框&#xff0c;点击登录对话框&#xff0c;如果账号和密码匹配&#xff0c;则弹出信息对话框&#xff0c;给出提示”登录成功“&#xff0c;提供一个Ok按钮&#xff0c;用户点击Ok后&#xff0c;关闭登录界面&#xff0c;跳转到其他界面 如果账号和密码不匹配&#xf…

01-你好Python-python环境安装 python解释器的安装 pycharm的安装

python环境安装 官方网址&#xff1a;https://python.org 这里可以下载最新版本的&#xff0c;下载完成以后在自己的浏览器文件下载的文件夹中找到该文件 下载速度可能会比较慢&#xff0c;这里已经提供好了文件&#xff0c;可以直接点击安装 点击Customize installation 点击…

pulsar的架构与特性记录

一、什么是云原生 云原生的概念是2013年Matt Stine提出的,到目前为止&#xff0c;云原生的概念发生了多次变更&#xff0c;目前最新对云原生定义为: Devps持续交付微服务容器 而符合云原生架构的应用程序是: 采用开源堆栈(K8SDocker)进行容器化&#xff0c;基于微服务架构提高灵…

人工智能利用深度学习技术增强高级驾驶辅助系统(ADAS)

深度学习通过实时传感器数据增强高级驾驶辅助系统(ADAS)&#xff0c;实现精确的物体检测、碰撞预测和主动决策。 人工智能和机器学习利用深度学习技术的优势&#xff0c;使高级驾驶辅助系统(ADAS)发生了重大变革。ADAS在很大程度上依赖深度学习来分析和解释从各种传感器获得的…

Flutter 中使用 ICON

Flutter Icon URL &#xff1a; https://fonts.google.com/icons&#xff1a; 在Flutter中使用 Icon 步骤如下&#xff1a; 导入图标库 在Dart 文件中导入 material.dart 包&#xff0c;该包包含了 Flutter 的图标库。 import package:flutter/material.dart;使用图标组件 …

救赎之道,就在其中

时光荏苒&#xff0c;不知不觉距离我踏入职场的第一天已经快一年了。最近也是看到平台举办年度征文活动&#xff0c;借此契机重新审视自己这两年来的成长历程&#xff0c;也希望对正在迷茫的人提供一些精神上的慰藉。 1.对未来的迷茫 如果要给两年前的自己打上标签&#xff0…

在IntelliJ IDEA上使用通义灵码(TONGYI Lingma)

参考链接&#xff1a; 通义灵码产品介绍_智能编码助手_AI编程_云效(Apsara Devops)-阿里云帮助中心 【IDEA如何使用通义灵码&#xff1f;】_idea 通义灵码-CSDN博客 1. 简介 1.1 定义 通义灵码&#xff0c;是阿里云出品的一款基于通义大模型的智能编码辅助工具&#xff0c;提…

实现多级缓存(Redis+Caffeine)

文章目录 多级缓存的概述多级缓存的优势 多级缓存的概述 在高性能的服务架构设计中&#xff0c;缓存是一个不可或缺的环节。在实际的项目中&#xff0c;我们通常会将一些热点数据存储到Redis或MemCache这类缓存中间件中&#xff0c;只有当缓存的访问没有命中时再查询数据库。在…

【UE Niagara学习笔记】06 - 制作火焰喷射过程中飞舞的火星

在上一篇博客&#xff08;【UE Niagara学习笔记】05 - 喷射火焰顶部的蓝色火焰&#xff09;的基础上继续实现喷射火焰的火星的效果。 目录 效果 步骤 一、创建材质实例 二、添加新的发射器 2.1 设置粒子材质 2.2 设置发射器持续生成粒子 2.3 设置粒子生成数量 2.4 设…

前端项目构建打包生成Git信息文件

系列文章目录 TypeScript 从入门到进阶专栏 文章目录 系列文章目录前言一、前端项目构建打包生成Git信息文件作用二、步骤1.引入相关的npm包1.1. **fs** 包1.2. **child_process** 包1.3. **os** 包 (非必须 如果你想生成的文件信息中包含当前电脑信息则可用)1.4. **path** 包…

MySql -数据库基本概念

一、数据库的基本概念 1.为什么要学数据库&#xff1f; 之前我们如果想将一些数据实现永久化存储&#xff0c;可以怎么做呢&#xff1f;没错。使用IO流的技术将数据保存到本地文件中但是接下来我有这样一个需求&#xff1a;将下面的user.txt文件中的王五年龄修改为35 张三 2…

视频智能剪辑方案,企业视频制作新时代

视频已经成为了人们获取信息、娱乐和学习的重要方式。然而&#xff0c;传统的视频制作过程繁琐且耗时&#xff0c;这对于许多企业来说无疑是一个巨大的挑战。为了解决这个问题&#xff0c;美摄科技凭借其在机器学习、深度学习等AI算法方面的深厚积累&#xff0c;自主研发了一套…

23111 IO进程线程 day8

使用信号灯集完成三个进程的同步&#xff0c;A进程输出字符A&#xff0c;B进程输出字符B&#xff0c;C进程输出字符C&#xff0c;要求输出结果为ABCABCABCABCABC... #include<myhead.h> #include "sem.h"int main(int argc, const char *argv[]) {pid_t pid…

Linux的网络服务DHCP

一.了解DHCP服务 1.1 DHCP定义 DHCP&#xff08;动态主机配置协议&#xff09;是一个局域网的网络协议。指的是由服务器控制一段IP地址范围&#xff0c;客户机登录服务器时就可以自动获得服务器分配的IP地址和子网掩码。默认情况下&#xff0c;DHCP作为Windows Server的一个服…

【开发小程序多少钱?智创开发】

开发一个小程序费用主要看做什么和怎么做&#xff1f; 第一部分&#xff1a;做什么&#xff1f; 做什么是指功能部分&#xff0c;开发的功能不一样&#xff0c;耗时也就不一样&#xff0c;价格自然也就不一样了。就好比买房&#xff0c;套二的公寓和别墅价格自然差距很大。所…

软光栅透视校正插值写好了

我这文章写的六,自己不写什么过程,直接发张图片.我发一下我看的引用. 透视矫正插值 Perspective-Correct Interpolation 计算机图形学六&#xff1a;正确使用重心坐标插值(透视矫正插值(Perspective-Correct Interpolation))和图形渲染管线总结 一开始写错了,改了大概两天改…

代理IP连接不上/网速过慢?如何应对?

当您使用代理时&#xff0c;您可能会遇到不同的代理错误代码显示代理IP连不通、访问失败、网速过慢等种种问题。 在本文中中&#xff0c;我们将讨论您在使用代理IP时可能遇到的常见错误、发生这些错误的原因以及解决方法。 一、常见代理服务器错误 当您尝试访问网站时&#…

Golang Web框架性能对比

Golang Web框架性能对比 github star排名依次: Gin Beego Iris Echo Revel Buffalo 性能上gin、iris、echo网上是给的数据都是五星&#xff0c;beego三星&#xff0c;revel两星 beego是国产&#xff0c;有中文文档,文档齐全 根据star数&#xff0c;性能&#xff0c;易用程度…

UGUI Image图像控件替换图片

代码为探索而来&#xff0c;不是最优代码&#xff0c;请按需使用。 Unity3d引擎版本&#xff1a;Uinty3d 20233.2.3f1 补充一下图片如何改成Texture2D&#xff1a; 1、将图片导入unity。 2、选择图片&#xff0c;按下图操作&#xff0c;点击应用即可。 脚本代码&#xff1a…

听劝,年度规划有它真的很必要!

2024年的时间进度条已走过一周&#xff0c;完成全年的1/52。 新年的flag悄然立下&#xff1a;愿逆风如解意&#xff0c;税后八个亿。 在不确定的世界中&#xff0c;发财暴富终归是确定的目标。 相比2023年的卷&#xff0c;年底的即兴生活正在悄悄上演&#xff0c;上一秒还在…