没有合适的资源?快使用搜索试试~ 我知道了~
CMU 15-819O 程序分析讲义.pdf
需积分: 5 0 下载量 68 浏览量
2024-02-03
12:13:14
上传
评论
收藏 1.62MB PDF 举报
温馨提示
试读
84页
CMU 15-819O 程序分析讲义
资源推荐
资源详情
资源评论
讲义笔记:WHILE语言和W
HILE 3A DDR表示
15-819O:程序分析
乔纳森·奥尔德里奇
jonathan.aldrich@cs.cmu.edu
第二讲
1 WHILE语言
在这门课程中,我们将学习使用一种名为WHILE的简单编程语言以及各种
扩展的分析理论。 WHILE语言至少与Hoare在1969年关于证明程序属性的逻
辑的论文一样古老(将在后面的讲座中讨论)。 它是一种简单的命令式语
言,具有对局部变量的赋值,if语句,while循环以及简单的整数和布尔表
达式。
我们将使用以下元变量来描述几个不同的语法类别。 左边的字母将被用
作表示程序的一部分的变量,而右边,我们描述变量表示的程序部分的类
型:
S 语句
一个 算术表达式
x,y程序变量
n 数字字面量
P 布尔谓词
WHILE语言的语法如下所示。 语句 S可以是一个赋值语句 x := a,一个
什么也不做的跳过语句(类似于C或Java中的单个分号或大括号),以及条
件为布尔谓词 P的if和while语句。 算术表达式 a包括变量 x,数字 n,以及
几个算术运算符,抽象地说
1
由 op一个表示。 布尔表达式包括true、f
a
lse、另一个布尔表达式的否定、
布尔运算符 op
b
应用于其他布尔表达式,以及关系运算符 op
r
应用于算术表
达式。
S ::= x := a
| 跳过
| S
1
; S
2
| 如果 P那么 S
1
否则 S
2
| 当 P执行 S
a ::= x
| n
| a
1
op
a
a
2
op
a
::= + | − | ∗ | /
P ::= 真
| 假
| 非 P
| P
1
操作
b
P
2
| a
1
操作
r
a
2
操作
b
::= 与 |或
操作
r
::= < | ≤ | = | > | ≥
2 WHILE 3A DDR:分析的一种表示
我们可以直接定义WHILE的语义,当然,在学习Hoare逻辑时我们会这样做
。
1
然而,对于程序分析来说,WHILE的源代码定义有些不方便。 即使是像
WHILE这样简单的语言也很难定义。 例如,WHILE有三种不同的语法形式
——语句、算术表达式和布尔谓词——我们需要分别定义每个语法的语义
。 更简单、更规则的程序表示将有助于简化我们的形式化过程。
作为起点,我们将消除递归算术和布尔表达式,并用简单的原子语句形
式替换它们,这些语句形式在类似于汇编语言指令之后被称为指令。 例如
,一个形如 w = x ∗ y + z的赋值语句
1Nielson等人的补充文本还定义了这里给出的WHILE语言的语义。
2
将被重写为一个乘法指令,后面跟着一个加法指令。
乘法指令将结果赋给一个临时变量 t
1
,然后在后续的加法指令中使用该变
量:
t
1
= x ∗ y
w = t
1
+ z
正如从表达式到指令的翻译所示,程序分析通常使用比源WHILE语言更
简单、更低级的程序表示进行研究。 通常,高级语言具有众多复杂的特性
,但可以简化为一组更简单的原语。 在更低的抽象级别上工作也支持编译
器的简洁性。
控制流结构,如if和while,同样被转换为更简单的goto和条件分支结构
,跳转到特定的(编号的)指令。 例如,形如if P then S
1
else S
2
的语句将
被转换为:
1 : if P then goto 4
2 : S
2
3 : goto 5
4 : S
1
5 : 程序的其余部分...
形如while P do S的语句的转换类似:
1 : if not P goto 4
2 : S
3 : goto 1
4 : 程序的其余部分...
这种形式的代码通常被称为3地址代码,因为每条指令都是一个简单的
形式,最多有两个源操作数和一个结果操作数。 现在我们定义从WHILE语
言产生的3地址代码的语法,我们将其称为WHILE3ADDR。 这种语言包括一
组简单的指令,用于将常量加载到变量中,从一个变量复制到另一个变量
,从两个变量计算出一个变量的值,或者跳转(可能有条件地)到一个新
地址n。 程序只是从地址到指令的映射:
3
I ::=
| 变量x赋值变量 y
| 变量x赋值变量y 运算符 z
| 跳转到行号 n
| 如果变量x 运算符 变
量
r
0跳转到行号n运算符 ::=
加 | 减 | 乘 |除变量
r
::= 小
于 ∈ Î ⇀ I
正式地定义从源语言(如WHILE)到较低级中间语言(如WHILE3ADDR
)的翻译是可能的,但对于编译器课程的范围来说,这更合适。 对于本课
程的目的,上述示例应该足够直观。 我们将首先在WHILE3ADDR中形式化
程序分析,然后更详细地研究其语义,以验证程序分析的正确性。
4
讲座笔记:用于数据流
分析的框架
WHILE 3ADDR
15-819O:程序分析
乔纳森·奥尔德里奇
jonathan.aldrich@cs.cmu.edu
第二讲
1 定义数据流分析
为了使数据流分析的定义准确,我们需要先研究数据流分析如何表示程序
的信息。 分析将在每个程序点计算一些数据流信息 σ。 通常 σ会告诉我们
关于程序中每个变量的一些信息。 例如, σ可能是从变量到某个集合 L中
的抽象值的映射:
σ P Var Ñ L
这里,L代表我们在分析中感兴趣的抽象值集合。 这会因不同的分析而
有所不同。 考虑零分析的例子,我们想要追踪每个变量是否为零。对于这
个分析,L可以表示集合 tZ, N, ?u。 在这里,抽象值 Z表示值0, N表示所
有非零值。
我们使用 ?用于我们不知道一个变量是否为零的情况。
从概念上讲,每个抽象值都代表了程序执行时可能出现的一个或多个具
体值的集合。 为了理解抽象值代表的含义,我们定义了一个抽象函数 α,
将每个可能的具体值映射到一个抽象值:
α : Ú Ñ L
1
剩余83页未读,继续阅读
资源评论
绝不原创的飞龙
- 粉丝: 1w+
- 资源: 1091
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功