运行和验证 hv6

时间  2019-12-18
标签 运行 验证 hv6 繁體版
原文   原文链接

目录html

运行和验证 hv6

@(hv6是Hyperkernel: Push-Button Verification of an OS Kernel中设计的一款操做系统,用这款操做系统实验了一种新的验证内核的方法,具体请查看这篇论文:Hyperkernel: Push-Button Verification of an OS Kernel)前端

运行 hv6

安装相关软件

Linux Ubuntu 17.10
Binutils 2.29.1
GCC 7.2.0
QEMU 2.10.1node

  • Binutils 2.29.1
  • 简介
    - GNU Binutils，即GNU Binary Utilities的简写，通常简称为 Binutils。   参考官网GNU Binutils的解释，能够解释为：GNU Binutils是一组二进制工具的集合。
    二进制此处主要指的是，源代码编译出来的目标(*.o)文件，(Linux下面的elf等)可执行文件等等。
    • Binutils主要包括了ld和as。
      - ld
         连接器。将多个目标文件，连接成一个可执行文件（或目标库文件）。
      - as
         汇编器。将汇编源代码，编译为（目标）机器代码
  • 安装 
    tar -xvf 
   make&make install
  • gcc
  • 源码安装参考连接

    • gcc默认是编译c89,可是c89不支持explict关键字，因此在make生成Makefile以后，须要修改Makefile中的-std=c89为-std=c99
      Alt textpython

      调试

  • 直接make会报undefined reference to 'static_assert'错
    • 解决：因为须要不存在的头文件<assert.h>,故删掉此assert
    [tianchiliu@localhost hv6]$ make
  GEN      o.x86_64/hv6/user/fs/mkfs
/tmp/ccfyijTc.o: In function `main':
mkfs.c:(.text+0xad): undefined reference to `static_assert'
collect2: error: ld returned 1 exit status
make: *** [o.x86_64/hv6/user/fs/mkfs] Error 1
  • make qemu会出现以下错误
    `qemu/target/i386/kvm.c:1849: kvm_put_msrs: Assertion `ret == cpu->kvm_msr_buf->nmsrs' failed.
    @(这个错误和VMware有关)
  • 解决方法不少,可参考qemu官方论坛,我hv6/Makefile中添加了QEMUOPTS += -cpu host,pmu=off
    @[QEMUOPTS += -cpu host,pmu=off不能在
    QEMUOPTS += -M q35,accel=$(QEMU_ACCEL),kernel-irqchip=split -cpu $(QEMU_CPU)上面，
    后者必须在配置中的最前面]
QEMU         := qemu-system-$(ARCH)<br>
QEMUOPTS     += -M q35,accel=$(QEMU_ACCEL),kernel-irqchip=split -cpu $(QEMU_CPU)<br>
QEMUOPTS     += -cpu host,pmu=off <br>
QEMUOPTS     += -serial mon:stdio -s<br>
QEMUOPTS     += -display $(QEMU_DISPLAY)<br>
QEMUOPTS     += -smp cpus=$(NR_CPUS)<br>
QEMUOPTS     += -device isa-debug-exit
QEMUOPTS     += -debugcon file:/dev/stdout
QEMUOPTS     += -netdev user,id=net0,hostfwd=tcp::10007-:7,hostfwd=tcp::10080-:80,hostfwd=tcp::5900-:5900<br>
QEMUOPTS     += -device $(QEMU_NIC),netdev=net0 -object filter-dump,id=filter0,netdev=net0,file=$(O)/qemu.pcap<br>
QEMUOPTS     += -device $(IOMMU),intremap=on<br>

  • 继续make qemu出现以下错误linux

    [   12.576076] kernel panic: hvm: no svm/vmx
    解决方法：开启kvm的虚拟化嵌套，宿主机开启虚拟化加上VMware勾选虚拟化只是支持VMware中的系统虚拟化，在qemu中运行系统就须要虚拟化嵌套了。参考连接
    • 首先检查 KVM host（宿主机/母机）上的kvm_intel模块是否打开了嵌套虚拟机功能
    [tianchiliu@localhost hv6]$ cat /sys/module/kvm_intel/parameters/nested
 N
    • 若是上面的显示结果不是 Y 的话须要开启 nested：
    [root@localhost hv6]# modprobe -r kvm-intel
[root@localhost hv6]# modprobe kvm-intel nested=1
[root@localhost hv6]# cat /sys/module/kvm_intel/parameters/nested
Y

    -- 最后make&make qemu,运行成功了！c++

    fs: use memfs
fs: size 1000 nblocks 904 ninodes 4000 nlog 30
ns: waiting for link to come up
ns: link up at 1000 Mb/s full-duplex
ns: MAC address in EEPROM
ns: ether 52:54:00:12:34:56
ns: no caplist
ns: dhcp initializing
ns: inet 10.0.2.15 netmask 255.255.255.0 broadcast 10.0.2.2
init: starting httpd
init: starting vncd
init: starting sh
httpd: waiting for http connections...
vncd: 1322 8x16 glyphs
vncd: waiting for vnc connections...
$
    • 测试
      在浏览器输入http://localhost:5900/sh.html.
      终端输出：
    vncd: client connected from 10.0.2.2
vncd: client version GET /sh.html



验证 hv6

安装相关软件

Linux Ubuntu 17.10
LLVM 5.0.0
Z3 4.5.0
Python 2.7.10

    安装了不少软件后，VMware提示容量不足，下面进行:git

  • VMware扩容：
  • 使用VM图形界面，关闭虚拟机，编辑虚拟机配置，直接将硬盘空间扩容。
  • 对新增长的硬盘进行分区
[root@localhost] fdisk /dev/sda　　　　
      p　　　　　　　查看已分区数量（我看到有两个 /dev/sda1 /dev/sda2）
      n　　　　　　　新增长一个分区
      p　　　　　　　分区类型咱们选择为主分区
      　　　　　　   分区号选3（由于1,2已经用过了，见上）
      回车　　　　　 默认（起始扇区）
      回车　　　　　 默认（结束扇区）
      t　　　　　　　修改分区类型
      　　　　　　   选分区3
      8e　　　　　　 修改成LVM（8e就是LVM）
      w　　　　　　  写分区表
      q　　　　　　  完成，退出fdisk命令
<tab><tab>&nbsp; &nbsp; &nbsp; &nbsp; 使用`partprobe` 命令 或者重启机器
  • 格式化分区
mkfs.xfs  /dev/sda3  #因为centos7默认是xfs系统,因此我选择了mkfs.xfs
  • .添加新LVM到已有的LVM组，实现扩容
lvm　　　　　　　　　　　　　   进入lvm管理
lvm>pvcreate /dev/sda3　　　这是初始化刚才的分区，必须的
lvm>vgextend cl /dev/sda3  将初始化过的分区加入到虚拟卷组centos (卷和卷组的命令能够经过  vgdisplay )            #cl是可经过vgdisplay查看,即第一行vg name
lvm>vgdisplay -v
lvm>lvextend -l+768 /dev/mapper/centos-root　　扩展已有卷的容量（768是经过vgdisplay查看的free的大小）我增长了3G
lvm>pvdisplay   查看卷容量，这时你会看到一个很大的卷了
lvm>quit    　退出

  • 以上只是卷扩容了，下面是文件系统的真正扩容
    CentOS 7 下面 因为使用的是 XFS，因此要用:
    xfs_growfs /dev/mapper/cl-root
    CentOS 6 下面 要用:
    resize2fs /dev/mapper/cl-rootgithub

    @[cl-root可根据查看挂载点信息命令df -h获得]
    参考连接
  • Z3 4.5.0
git clone https://github.com/Z3Prover/z3.git
cd z3
python scripts/mk_make.py
cd build
make
sudo make install

参考连接

bootstrap

  • cmake
    LLVM 5.0.0不支持./configure&make,须要安装cmake，故安装cmake：
    参考连接1

    由于参考连接1中./configure时报错没法解决，


    遂使用下面./bootstrap方法
    参考连接2
    ./bootstrap提示glibc没有GLIBCXX_3.4.21或更高版本centos

    • 核实版本问题：
    [root@localhost cmake-2.8.12.2]  strings /usr/lib64/libstdc++.so.6 | grep GLIBCXX
    咱们看到当前GCC版本中的确没有GLIBCXX_3.4.15,考虑到刚安装过新版的GCC,彷佛不该该出现这样的问题。

    • 顺着gcc安装路径，找到了新的libstdc++：
    [root@localhost cmake-2.8.12.2] strings /usr/local/lib64/libstdc++.so.6.0.24|grep GLIBCXX
    @[libstdc++.so.6.0.24要去/usr/local/lib64/具体查看是否存在]
    • 把这份软链到/usr/lib64/
    [root@localhost cmake-2.8.12.2] cp /usr/local/lib64/libstdc++.so.6.0.20 /usr/lib64/
[root@localhost cmake-2.8.12.2] cd /usr/lib64/
[root@localhost lib64] rm -f libstdc++.so.6
[root@localhost lib64] ln -s libstdc++.so.6.0.20 libstdc++.so.6
[root@localhost lib64] ll libstdc*
lrwxrwxrwx. 1 root root      19 5月  12 13:34 libstdc++.so.6 -> libstdc++.so.6.0.20
-rwxr-xr-x. 1 root root  987096 11月 22 02:08 libstdc++.so.6.0.13
-rwxr-xr-x. 1 root root 6700716 5月  12 13:33 libstdc++.so.6.0.20
            参考连接
    • 安装
    ./bootstrap
 gmake
 make install
    cmake基本命令格式为：cmake (cmakelist所在目录) (配置)
  • LLVM 5.0.0


    LLVM 是 Low Level Virtual Machine 的简称，这个库提供了与编译器相关的支持，可以进行程序语言的编译期优化、连接优化、在线编译优化、代码生成。
    clang官网的介绍能够看出，clang的目标是建立一种新的基于C语言的LLVM编译器的前端（应该是提供词法分析、语法检测等功能）
    • 1 下载编译所需的文件
    [root@typecodes ~]# wget -c http://releases.llvm.org/4.0.1/llvm-4.0.1.src.tar.xz
[root@typecodes ~]# wget -c http://releases.llvm.org/4.0.1/cfe-4.0.1.src.tar.xz
[root@typecodes ~]# wget -c http://releases.llvm.org/4.0.1/clang-tools-extra-4.0.1.src.tar.xz
[root@typecodes ~]# wget -c http://releases.llvm.org/4.0.1/compiler-rt-4.0.1.src.tar.xz
[root@typecodes ~]# wget -c http://releases.llvm.org/4.0.1/libcxx-4.0.1.src.tar.xz
[root@typecodes ~]# wget -c http://releases.llvm.org/4.0.1/libcxxabi-4.0.1.src.tar.xz
[root@typecodes ~]# wget -c http://releases.llvm.org/4.0.1/libunwind-4.0.1.src.tar.xz
    • 2 解压全部文件到目录：llvm
      • 解压 llvm-4.0.1.src.tar.xz
      [root@typecodes ~]# tar -xf llvm-4.0.1.src.tar.xz && mv -f llvm-4.0.1.src llvm && rm -rf llvm-4.0.1.src.tar.xz
      • 解压 cfe-4.0.1.src.tar.xz
      [root@typecodes ~]# cd llvm/tools/ && mv ~/cfe-4.0.1.src.tar.xz .
   [root@typecodes tools]# tar -xf cfe-4.0.1.src.tar.xz && mv -f cfe-4.0.1.src clang && rm -rf cfe-4.0.1.src.tar.xz
      • 解压 clang-tools-extra-4.0.1.src.tar.xz
      [root@typecodes tools]# cd clang/tools/ && mv ~/clang-tools-extra-4.0.1.src.tar.xz .
   [root@typecodes tools]# tar -xf clang-tools-extra-4.0.1.src.tar.xz && mv -f clang-tools-extra-4.0.1.src extra && rm -rf clang-tools-extra-4.0.1.src.tar.xz
      • 进入projescts目录
      [root@typecodes tools]# cd ../../../projects/ && pwd
/root/llvm/projects
      • 解压 compiler-rt-4.0.1.src.tar.xz
      [root@typecodes projects]# mv ~/compiler-rt-4.0.1.src.tar.xz .
  [root@typecodes projects]# tar -xf compiler-rt-4.0.1.src.tar.xz && mv -f compiler-rt-4.0.1.src compiler-rt && rm -rf compiler-rt-4.0.1.src.tar.xz
      • 解压 libcxx-4.0.1.src.tar.xz
      [root@typecodes projects]# mv ~/libcxx-4.0.1.src.tar.xz .
 [root@typecodes projects]# tar -xf libcxx-4.0.1.src.tar.xz && mv -f libcxx-4.0.1.src libcxx && rm -rf libcxx-4.0.1.src.tar.xz
      • 解压 libcxxabi-4.0.1.src.tar.xz
      [root@typecodes projects]# mv ~/libcxxabi-4.0.1.src.tar.xz .
[root@typecodes projects]# tar -xf libcxxabi-4.0.1.src.tar.xz && mv -f libcxxabi-4.0.1.src libcxxabi && rm -rf libcxxabi-4.0.1.src.tar.xz
      • 解压 libunwind-4.0.1.src.tar.xz
      [root@typecodes projects]# mv ~/libunwind-4.0.1.src.tar.xz .
[root@typecodes projects]# tar -xf libunwind-4.0.1.src.tar.xz && mv -f libunwind-4.0.1.src libunwind && rm -rf libunwind-4.0.1.src.tar.xz

    • 建立CMake的编译目录：build

      [root@typecodes projects]# cd ~/ && mkdir build && cd build/
      • 使用Cmake编译生成makefile文件
      [root@typecodes build]# cmake ../llvm -G "Unix Makefiles" -DCMAKE_C_COMPILER=gcc -DCMAKE_CXX_COMPILER=g++ -DCLANG_DEFAULT_CXX_STDLIB=libc++ -DCMAKE_BUILD_TYPE="Release" ../llvm
      cmake ../llvm：找到cmakelist所在目录

  • 开始经过make命令编译


    因为llvm对硬件要求特别高，因此使用make -j2来编译
    此处不使用make -j4或make -j8由于只给虚拟机分配了3个处理器

    • 多核处理器下提升make的效率
      - make:使用单核编译
      - make -j[n]:在同一时间并行编译n个任务
      - make -j:不限制同一时间并行编译的任务数
      - make -j2:通常双核处理器使用
      - make -j4:4核处理器
      -


      n具体是多少还要根据要编译的项目来定，和处理器个数没有必然关系


      make -j命令并非任何状况下均可以用的，在存在编译依赖的状况 下，单核编译仍是一种比较稳妥的方案。

在4G内存、3核处理器下，编译LLVM用时5h

  • 安装 clang 和 llvm
    make install


    出现 clang cannot copy /user/local/build/c-text to /user/local/bin，手动将其复制到/user/local/bin



    安装成功,测试下
    ```
    [root@localhost tianchiliu]# llvm-config --version
    4.0.1
-  安装clang/clang++所须要的libc++库
      `make install-cxx install-cxxabi`
      
- `make hv6-verify`
:Runs the verification scripts for the hv6 kernel. This includes building the kernel into LLVM IR, translating the kernel to Python using Irpy, and invoking hv6/spec/main.py
出现以下错误:

irpy/compiler/PyLLVMEmitter.cc: In member function ‘void irpy::PyInstVisitor::visitSwitchInst(llvm::SwitchInst&)’:
irpy/compiler/PyLLVMEmitter.cc:546:49: error: passing ‘const llvm::SwitchInst::CaseIteratorT<llvm::SwitchInst, llvm::ConstantInt, llvm::BasicBlock>’ as ‘this’ argument discards qualifiers [-fpermissive]
``解决: 把 545行 for (const `auto &c : i.cases()) 改成for (auto &c : i.cases()) {,即去掉const

分析：C++中，const 修饰的参数引用的对象，只能访问该对象的const函数，由于调用其余函数有可能会修改该对象的成员，编译器为了不该类事情发生，会认为调用非const函数是错误的。
通常有三种解决方法：

  • 把非const函数改成const
  • 把const修饰的参数的const去掉

  • 编译时加上-fpermissive忽略掉const可能引起的安全问题

  • make hv6-virify
  • 报错：
[root@localhost hv6]# make hv6-verify
    C++      o.x86_64/irpy/compiler/PyLLVMEmitter.o
    C++      o.x86_64/irpy/compiler/irpy.o
    C++      irpy/compiler/irpy
    IRPY     o.x86_64/hv6/hv6.py
Parsing took 70 ms.
Emitting took 24320 ms.
    PY2      hv6-verify
Traceback (most recent call last):
 File "o.x86_64/hv6/hv6py/kernel/spec/main.py", line 23, in <module>
   import libirpy
 File "/home/tianchiliu/hv6/irpy/libirpy/__init__.py", line 17, in <module>
   from ctx import newctx, initctx
 File "/home/tianchiliu/hv6/irpy/libirpy/ctx.py", line 18, in <module>
   import util
 File "/home/tianchiliu/hv6/irpy/libirpy/util.py", line 20, in <module>
   import z3
ImportError: No module named z3
  • 解决：查看z3 build中的example.py中的内容:
    • 由于4.8版本中没有bin目录，要将bin改成build
    • MYZ3为Z3的安装目录,例如个人完整路径为/usr/local/z3/build


      Running this example on Linux:
      export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:MYZ3/bin
      export PYTHONPATH=MYZ3/bin/python
    vi  ~/.bashrc
 export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/usr/local/z3/build
 ldconfig
    vi  /etc/profile
  export PYTHONPATH=/usr/local/z3/build/python
 source /etc/profile
    参考连接

  • 再次make hv6-verify:
    [root@localhost hv6]# make hv6-verify PY2 hv6-verify Using z3 v4.8.0.0 .....
    4G内存，3核处理器验证用时20h时提示:

    Traceback (most recent call last):
File "o.x86_64/hv6/hv6py/kernel/spec/main.py", line 590, in setUp
  self.solver = Solver()
File "/home/tianchiliu/hv6/irpy/libirpy/solver.py", line 58, in __init__
  stdin=subprocess.PIPE,
File "/usr/lib64/python2.7/subprocess.py", line 711, in __init__
  errread, errwrite)
File "/usr/lib64/python2.7/subprocess.py", line 1224, in _execute_child
  self.pid = os.fork()
OSError: [Errno 12] Cannot allocate memory
    • 分析:OSError: [Errno 12] Cannot allocate memory:超过最大线程数
      Linux doesn't have a separate threads per process limit, just a limit on the total number of processes on the system
  • 解决:
    cat /proc/sys/kernel/threads-max : 查看 echo 222222 > /proc/sys/kernel/threads-max 设置新的线程数
    参考连接

  • make irpy/test: Runs the Irpy test suite, which compares symbolic execution results to running the C code directly.
    • 报错：
    cd irpy/o.test && python2 test.py 
Random seed: 5075005128484348075
.[param.7 = 2084980470, param.6 = 2143437557]
In function irpy/test/add_overflow.c:test:24:14 
.................  In function irpy/test/poison_cond.c:test:23:9 
.........[i32 10, i32 10, i32 11, i32 12, i32 13, i32 14, i32 15, i32 _1, i32 _1, i32 703]
E...[param.140 = 0]
In function irpy/test/zero_div.c:test:23:14 
ERROR: test_switch_table (__main__.IRPyTest)
Traceback (most recent call last):
File "test.py", line 78, in <lambda>
 self._test(name, *args)
File "test.py", line 150, in _test
 self._test_o(name + '_1', *args)
File "test.py", line 136, in _test_o
 smt, symbolic_params = self._irpy(name, *args)
File "test.py", line 123, in _irpy
 libirpy.initctx(ctx, module)
File "/home/tianchiliu/hv6/irpy/o.test/libirpy/ctx.py", line 159, in initctx
 module._init_globals(ctx)
File "/home/tianchiliu/hv6/irpy/o.test/switch_table_1.py", line 14, in _init_globals
 irpy.declare_global_constant(ctx,'@switch_table',itypes.parse_type(ctx,'[10 x i32]*'),irpy.constant_data_array(ctx,itypes.parse_type(ctx,'[10 x i32]'),'[i32 10, i32 10, i32 11, i32 12, i32 13, i32 14, i32 15, i32 _1, i32 _1, i32 703]',),itypes.parse_type(ctx,'[10 x i32]'))
File "/home/tianchiliu/hv6/irpy/o.test/libirpy/z3eval.py", line 323, in declare_global_constant
 for n, i in enumerate(util.parse_constant_array(value)):
File "/home/tianchiliu/hv6/irpy/o.test/libirpy/util.py", line 265, in parse_constant_array
 return [int(v.split()[1]) for v in values[1:-1].split(', ')]
ValueError: invalid literal for int() with base 10: '_1'
Ran 33 tests in 87.651s
FAILED (errors=1)
make: *** [irpy/test] Error 1

  • 解决:
    ValueError: invalid literal for int() with base 10: '_1':字符串不能转为整型
    由 File "/home/tianchiliu/hv6/irpy/o.test/switch_table_1.py", line 14, in init_globalsirpy.declare_global_constant(ctx,'@switch_table',itypes.parse_type(ctx,'[10 x i32]*'),irpy.constant_data_array(ctx,itypes.parse_type(ctx,'[10 x i32]'),'[i32 10, i32 10, i32 11, i32 12, i32 13, i32 14, i32 15,**i32 _1, i32 _1**, i32 703]',),itypes.parse_type(ctx,'[10 x i32]'))：
    和
    [int(v.split()[1]) for v in values[1:-1].split(', ')]


    修改switch_table_1.py和switch_table_1.py的 line 14中**i32 _1, i32 _1为i32 1, i32 1**

  • 再次make irpy/test
    [root@localhost hv6]# make irpy/test cd irpy/o.test && python2 test.py Random seed: 17799494710820576461 .[param.7 = 2084980470, param.6 = 2143437557] In function irpy/test/add_overflow.c:test:24:14 ................. In function irpy/test/poison_cond.c:test:23:9 .........[i32 10, i32 10, i32 11, i32 12, i32 13, i32 14, i32 15, i32 1, i32 1, i32 703] [i32 10, i32 10, i32 11, i32 12, i32 13, i32 14, i32 15, i32 1, i32 1, i32 703] ....[param.141 = 0] In function irpy/test/zero_div.c:test:23:14 .. Ran 33 tests in 89.920s OK
    成功！

相关文章
相关标签/搜索
每日一句
    每一个你不满意的现在，都有一个你没有努力的曾经。
本站公众号
   欢迎关注本站公众号,获取更多信息
联系我们 最近搜索 最新文章 沪ICP备13005482号-10 MyBatis教程 SQL 教程 MySQL教程 Java 教程 Thymeleaf 教程 Hibernate教程 Spring教程 Redis教程