PDF 是自学者的噩梦,读 Anders 的 Static Program Analysis 窒息

2023-03-19 16:11:58 +08:00
 andyJado

卡在第 29 页的 exercise 3.3 两天了,没有任何办法,就硬搁这悟呐?

4191 次点击
所在节点    程序员
27 条回复
cc666
2023-03-20 00:28:52 +08:00
不知道这和 PDF 有什么关系?
如果是不能复制的话,不是 PDF 的问题,而是制作 PDF 的作者用的不是文字而是图片的原因,自己用 Adobe 之类的工具进行扫描优化就行了,也可以用到的时候再 OCR ,没法跳转可能是你没有加标记。
PS:这些都是很容易就能搜到的解决方法。
andyJado
2023-03-20 08:54:50 +08:00
@ufo5260987423 我的对象语言,一个文件会有几万行。我觉得我需要先趴到 CST 然后再趴 AST ,我抄的是 rust-analyzer 。你的索引是按函数建立的吗, 一个文件 10 个函数,编辑一个函数的时候只更新那个函数?
ufo5260987423
2023-03-20 08:59:47 +08:00
@andyJado #22 一个文件有几万行……用 vscode 打开都没法语法渲染了吧……
1 、我现在是按照文件更新的;
2 、如果一个文件几万行,且 10 个函数,那一个函数平均几千行代码,笑。
3 、我不能确定你的修改是否只对函数内部的语义有影响,如果你确定的话,把更新索引的粒度下降到函数也是可以的。
vcbal
2023-03-20 17:52:38 +08:00
@andyJado 额 你要是数学学的不错为什么没有想到向量呢?矩阵向量
andyJado
2023-03-21 08:28:21 +08:00
@vcbal 假设我想到了,能帮我理解“Int”和“上箭头 + Int”的区别吗?
DianQK
2023-03-21 09:55:52 +08:00
这刚好是我今年计划看的一本书,我试着把这块的看了,上箭头 int 就是指 int 的指针类型。
但 Exercise 3.3 我也看不明白要说啥。 似乎是说 TypeVar 这种 regular type (大概是说符合书中描述的规则的类型?)里面的 t 是不确定的,然后设计一个状态机可以用来判断两个类型是否相同?(不懂)
不过我重新翻了一下之前的版本,Types 这个章节就是一页带过,至少对我来说,这一章不是静态分析的关键内容。跳过这一章看后面的应该没啥问题。如果是我,我选择跳过不懂的这部分。

pdf 倒是我最喜欢的一种格式了,高保真&可离线。也可以跳转的,取决于作者写不写吧。我看 spa 这本又不少可以跳转的地方。或者是 OP 下载地址不对? https://cs.au.dk/~amoeller/spa/

除了跳过,还可以直接问作者呀。我发了邮件,不过还没回复我。
DianQK
2023-03-23 21:16:26 +08:00
我可以肯定的说,OP 你可以忽略这个习题,因为作者回复我了,说这是个不重要的习题。我跟随作者给出的一些提示 /答案,总结大概如下(我的理解不一定对):

首先我可以肯定,这是将自动机( FA )相关的问题,前置知识在龙书的第 3.6 小节(不推荐看网上的一些介绍,感觉没有龙书写的详细易懂)。Type Analysis 虽然也是静态分析?但通常提到的静态分析对应的应当是本书后面章节的内容。Type Analysis 应该划分为另一个范畴了吧,我觉得忽略这章看本书更合适一些。

这里一直提到的 language 翻译过来虽然是语言,但我觉得解释为句子 /一段话更贴切一些。比如“很高兴见到你”,这是一段话,也是中文(对应的 language )。
所以这里说的就是正则语言(表达式),只不过不是平常理解的正则表达式,而是更通用的概念。即符合某种正确规则的具体描述语言(一段话)。

抱歉,我没有继续把龙书的 3.7-3.9 看了,这几节应该是讲 FA 的应用部分。Ex 3.3 也**只是说怎么把定义的各种类型画成对应的 FA**,至于啥用,我不知道。作者回我的图片很模糊,感觉不是标准的 FA 。(抱歉,我不能直接贴这张图,因为我忘记了要一份授权,但我基于自己的理解重新画一遍应该没问题吧。)

OP 你把 3.6 小节看了之后,应该就可以了解底下的内容(如果没有,那一定是我转述 /理解的不对)。

画出来的 FA 如图:


有些字符我还不知道怎么打出来,就平替一下。这里 FA 用来判断能否接受一个描述对应类型的语言。
一些设定:
- 虚线圈似乎表示这里可以自由发挥 /匹配,什么类型都可以接受
- 1 、2 、3 数字用来表示状态转换的顺序 /参数?,当遇到一个 TypeVar ( t )时候,回到初始状态按照数字顺序匹配
- ut.(&int, t)->int 中的 t 是受限(递归的)的,t 必须满足自身的 (&int, t)->int 类型,这种时候可以回到初始状态接着匹配

所以图中的 FA 可以接受 ut.(&int, t)->int ,首先匹配参数 1 ,&int 成功,然后参数 2 是 t 回到开始状态,参数 3 直接一个 int 结束。

这是一个专为移动设备优化的页面(即为了让你能够在 Google 搜索结果里秒开这个页面),如果你希望参与 V2EX 社区的讨论,你可以继续到 V2EX 上打开本讨论主题的完整版本。

https://www.v2ex.com/t/925298

V2EX 是创意工作者们的社区,是一个分享自己正在做的有趣事物、交流想法,可以遇见新朋友甚至新机会的地方。

V2EX is a community of developers, designers and creative people.

© 2021 V2EX