Blog Test
0%

毕设日志

Posted on Edited on

2022-03-25

完成 getArrayElementExpr() mkStoreConstraint() mkLoadConstraint() 的FP相关编码.

目前的问题:

  • assert(L179) fail : arrayIndex超标. 2个疑惑: 为什么index的单位似乎是byte, 而不是sizeof(float). 为什么index会越界.
  • 测试样例int和float的表现不一致

可能的解决方向:

  • 了解路径遍历的机制, 探究为什么会遍历到index越界的路径
  • 已经编码的实现错误, 或更多的地方需要编码

接下来的任务:

  • z3的表达式类型
  • llvm IR
  • malloc时对堆区的建模(InstParser)
  • 指针相关验证的学术界方法(看论文)

2022-03-28

确定了brick的main branch存在的bug，设计了第一个测试样例。

往期问题解答：

  • int和float的表现不一致：minisat给出的结果不一致（BoundedVerifier:L285），后续线索中断。
  • arrayIndex越界，这是一个bug！目前已知其存在于commit 31389c1中。

预备向上问题报告：

  • BVVerifier:L186的assert单位不一致吧，arrayIndex单位是sizeof(type)，memSize单位是byte。导致这个问题的bug可能原生存在于commit 31389c1。（已报告）
  • 为什么int类型数组的测试样例总是报告minisat.solver.FALSE导致可以不进入BVVerifier的solver。（未报告，觉得意义不大）
  • brs1f.c验证时报告!=INTNUM的assert，是因为不想做malloc(变量)吗。（已报告）

遇到的问题和意向解决方法：

  • 确定从哪个分支开始编码：
    测试用例：

      brs1.c 观察assert !=INTNUM
  test_case_brs1.c 观察assert ArrayIndex out of bound

    （已解决，最新分支，等待学长完成debug）

  • 规避assert限制：
    取消编译优化
    （已解决，等待学长给找测试样例，因为旧的测试针对的是memmory safety，而需要的测试是数值计算相关的）

  • test_case_brs1_f-A.c 为什么会FAIL，理论上.ll：L71处的跳转不应实现
    那么，是否是cfg的path生成有问题？
    （已解决，因为N可能<0）

  • 为什么int类型数组的测试样例总是报告minisat.solver.FALSE，minisat.solve做了什么？
    TODO 未解决！

2022-03-29

阅读了instParser的parseCall中的malloc部分处理代码，该部分代码将IR表达成Constraint。
「批注」实际上，是要看InstParser和mkMallocConstraint，况且目前的代码仅仅对malloc(常数)的情况做了建模，真正艰巨的任务还没有完成。

找了一些中文文献，没有找到对内存建模的新颖描述。令，多关于内存安全验证，但应寻找数值计算的文献。

预备向上报告：

  • BVVerifier::mkMallocConstraint中heapMemory的memSize应该直接取llvm ir中call malloc的参数吗？参数的单位是字节，但这里似乎不需要字节。（未报告：暂时不去管这里，memSize直接取字节比较方便，但是getArrayElementExpr中使用时要谨慎，似乎有的代码不对，要改，等最新版代码出来，再做定夺）

遇到的问题和意向解决方法：

  • heapMemory::memSize为什么需要是Variable*类型，这里似乎用uint32_t就够了？
    (已解决：因为这是个表达式啊)

2022-04-01

parseAllocaInst部分FP相关编码。
mkGetPtrExpr函数var1.size==1时FP相关编码。
mkMemStoreConstraint中FP相关代码修改。
测试用例data_structures_set_malloc_f.c通过（获得SUCCESS和FAIL的结果）。

预备向上报告：

  • 为什么mkGetPtrExpr函数var1.size==1时FP相关编码和INT部分完全一致即可？如若如此，为什么要分类？

  • memmory check时alloc指令未实现？

2022-04-26

(其实4月初也有通过测试样例 data_structures_set_malloc.c 和 data_structures_set_malloc_f.c, 以及提交中期报告啊…)

在更新了学长的最新提交后, 仍确认data_structures_set_malloc.c, data_structures_set_malloc_f.c通过

2022-05-01

(躺平了3个星期之后终于开始干活了…)

自己实现一遍malloc, 方法是解析函数my_malloc, 测试brick是否工作正常. 测试样例test_my_malloc/my_malloc_i.c和test_my_malloc/my_malloc_f.c由data_structures_set_malloc.c和data_structures_set_malloc_f.c修改而来. 未实现功能时, 运行测试样例产生段错误; 完成框架代码后(8个文件, 27行代码), 运行测试样例仍产生段错误; 完成全部代码(8个文件, 133行代码), 通过测试样例.

store遇到循环时的处理, 尚未发现可以误触FAIL的测试样例, 没有查看.ll源码看是否有循环. 认为: 看是否真的重复生成了store相关的约束应该在生成约束时打印z3表达式, 然后比对是否存在如”x1==x2, x1==x3”的约束.

2022-05-02

找store遇到循环时的样例，需要兼顾“llvm ir中编译出malloc函数”，“对数组元素的操作在llvm ir中编译出store指令”。但目前未找到遇到循环的样例。loop_3.c样例中有store操作（offset已知）出现循环，但exprl和exprr均为相同的变量，此处可以深挖，即exprr是如何来的，其来源可能是随机的。loop_3.c加了一个大循环，似乎失败。尝试在data_structures_set_malloc.c修改得到测试样例，失败，原因是原样例过于复杂，不易判断是否对相同数组元素进行了多次store操作，但是后来发现还是可以进行下去的。

loop_4.c突破：main.%0 Pointer = store main.call23 Int约束出现两次，其中call23均为“=NONDET”，但生成z3约束时均为exprl: |Brick.ARRAY.HEAPMEM:0.element:0| exprr: main.call23_0，需要探究，为何右侧约束名字都一致，是不是生成z3约束时细节有问题，即求exprr时，是否由于名字相同，直接去z3表达式数组中去找了。这种情况对于store虽然没错，但别的操作会不会有问题？能否找到反例？

loop_5.c找到一个不相关的bug：如果将SIZE改为100会报SUCCESSFUL但实际应为FAILED，后续应下载最新brick代码，编译后测试该bug是否还存在，避免是本地分支错误修改代码所致。又发现一个bug：写在loop_5_bug.c里了。loop_5_bug_2.c在提交40a88ea1上关闭memoryBoundCheck后FAILED，但我认为应该是SUCCESSFUL的。

目前的计划是在历史某个main的提交上找到一个没有store循环操作时表现正常的样例，然后测试其在有store循环时是否产生FAILED或者程序运行错误等，若是SUCCESSFUL，则要观察是否是假SUCCESSFUL(即找出报SUCCESSFUL的原因，是真的考虑到了store操作可能在循环中的情况，还是没有考虑到这种情况，但巧合报SUCCESSFUL了)。如果这条路走不通，也可以先实现处理store在循环中的代码，至于测试样例，后面再说。

2022-05-03

按照自己的理解实现了heapMemory部分的循环中出现store指令的brick代码，但苦于找不到测试样例，这部分准备求助学长。

需要写论文了，先写大纲，然后写文献综述。

2022-05-04

去网上找论文。

初始化了论文模板NJU Thesis，写了论文大纲。

2022-05-06

整理了论文写作的经验，发现了形式化方法领域的几篇好综述（中文），撰写了论文的绪论部分（截止目前论文3208字）。

2022-05-07

研究现状的程序验证部分、有界模型检验部分，写了共1000字左右。

找了大量的与指针/内存建模相关的形式化/程序验证等相关的文章。【内存模型】参考代子季，李齐军的学位论文。

写到章节3.1左右（字数6474)。

2022-05-08

字数7500。

2022-05-11

写4.1，字数8324。
写4.2，字数9559。
写4.3，字数10650。
写4.4，字数11013。

2022-05-12

写5.0，字数11308。
写5.1，字数13192。
写5.2,5.3，字数14542。

写6，字数15037。

2022-05-13

写参考文献

2022-05-14

修改完一遍正文，15293字。
中文摘要，15709字。
英文摘要，15983字。
附录。
致谢，16396字。

2022-05-18

修改第四章，设计。

2022-05-19

修改第四章。

2022-05-20

修改第四章。（校庆快乐！）

2022-05-21

修改第四章完成。

论文修改一遍（v0.2，17893字），通过知网查重（0.9%）。

2022-05-31

论文修改第二遍（v0.3，20239）。

修改了摘要，增加了篇幅。
增加了1.2节，相关工作介绍。
原1.2和1.3节合并为现1.3节。
原第二章第三章合并为现第二章，背景知识。
为3.3节增加了算法和流程图。
增加3.3.4小节，验证案例。
增加4.2.3小节，对比实验。
修改了其他细节。

2022-06-16

提交终稿，泛泛而谈前人的工作
（v0.6，20414）。

答辩准备

熟悉重要类的域，明白每个域的含义
熟悉各个函数的代码，明白每行代码的含义
要将论文中的图、数学公式、伪代码与实际的C++代码建立联系

论文写作

  • todo
    • 绪论中的balabala
    • 第一章工作流程插图
  • 观点
    • 软件技术蓬勃发展，应用面十分广泛（是不是可以顺带提一句C语言）
    • 软件正确性很重要
    • 软件正确性很难保证（为什么？开发流程，软件的性质.代码量易于激增，判断软件是否正确本身就是难事）
  • 方法
    • 普适方法
      • 适时举例子
      • 剖析原因
    • 背景、研究现状
      • 分析同种类别的其他技术（如 软件验证 vs 软件测试）对方是什么，有哪些分类，如何工作，有哪些优点和不足，什么时候会有不足，不足是因为什么造成的。我们的方法历史源头，理论基础，主要分类；不同类别技术如何诞生的，工作原理介绍（尤其是如何生效的部分，如发现违反性质的行为），技术可以产生什么结果。
    • 目的、流程、方法
      • 别人的思路、手段，有哪些局限性（举例子），会导致什么后果（如精读不高、速度不够）
      • 本文做了什么（分点写，提出了什么方法，实现了什么工具）
      • 文章组织结构（技术介绍，提出xx方法，实现xx系统+实验，总结展望）

TO DO

  • 写论文
  • store遇到循环怎么办, 先找到一个本不应fail却fail了的测试样例(注意应查看.ll源码, 确认真的path中有循环), 再编码解决问题
  • FP相关代码有些混乱，找到所有stupidpanther提交的代码，逐一落实代码的作用，判断写的对不对，查看04-01发现的bug情况。
  • 再写几个测试样例（最好包含 FAIL 和 SUCCEED，样例test_case_brs1_f-B.c实现了触发assert ArrayIndex bound）
  • 指针相关验证的学术界方法(看论文)（理解PPT创新点与难点1.2.）关键点：当malloc参数是变量时，如何建模？如何让heapMemory::memSize的类型为Variable*这个伏笔真正发挥作用？
    「批注」可以找程序堆建模的文献的参考文献
  • z3的表达式类型（目的是理解PPT创新点与难点3.）
  • llvm IR
  • solveSAT是基于路径遍历的吗
  • reorderPath（在BoundedVerifier:L288被引用）是做什么用的