運行和驗證 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教程