运行和验证 hv6

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

运行 hv6

运行和验证 hv6
- 运行 hv6
  - 安装相关软件
  - 调试

安装相关软件

Linux Ubuntu 17.10
Binutils 2.29.1
GCC 7.2.0
QEMU 2.10.1

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

调试

直接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[官方论坛](http://qemu.11.n7.nabble.com/Bug-1661386-NEW-Assertion-ret-cpu-gt-kvm-msr-buf-gt-nmsrs-failed-td462940.html#a463422),我hv6/Makefile中添加了`QEMUOPTS     += -cpu host,pmu=off`
@[`QEMUOPTS     += -cpu host,pmu=off`不能在
`QEMUOPTS     += -M q35,accel=$(QEMU_ACCEL),kernel-irqchip=split -cpu $(QEMU_CPU)`上面，
后者必须在配置中的最前面]

```cpp
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出现如下错误

[ 12.576076] kernel panic: hvm: no svm/vmx

解决方法：`开启kvm的虚拟化嵌套`，宿主机开启虚拟化加上VMware勾选虚拟化只是支持VMware中的系统虚拟化，在qemu中运行系统就需要虚拟化嵌套了。[参考链接](https://www.cnblogs.com/wucg/p/8587257.html)
- 首先检查 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`,**运行成功了！**

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


<br><br>
##验证 hv6
###安装相关软件
   Linux Ubuntu 17.10
   LLVM 5.0.0
   Z3 4.5.0
   Python 2.7.10    
&nbsp; &nbsp; 安装了很多软件后，VMware提示容量不足，下面进行:
- `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-root` 

  @[cl-root可根据查看挂载点信息命令`df -h`得到] 
[参考链接](http://www.vpswe.com/linux/406.html)
- 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

  [参考链接](http://blog.sina.com.cn/s/blog_15aacc1fd0102ym55.html)
<br>

- **cmake**
`LLVM 5.0.0`不支持`./configure&make`,需要安装`cmake`，故安装cmake：<br>  [参考链接1](https://www.cnblogs.com/zychengzhiit1/p/5628711.html)<br>
	因为参考链接1中`./configure`时报错无法解决，<br><br>
	遂使用下面`./bootstrap`方法<br>[参考链接2](https://blog.csdn.net/lj402159806/article/details/76408597)
	`./bootstrap`提示glibc没有`GLIBCXX_3.4.21`或更高版本

  - 核实版本问题：

[root@localhost cmake-2.8.12.2] strings /usr/lib64/libstdc++.so.6 | grep GLIBCXX

    我们看到当前GCC版本中的确没有GLIBCXX_3.4.15,考虑到刚安装过新版的GCC,似乎不应该出现这样的问题。<br><br>
 - 顺着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

&nbsp; &nbsp;	 &nbsp; &nbsp;	[参考链接](https://www.cnblogs.com/weinyzhou/p/4983306.html) 
  - 安装

 ./bootstrap
gmake
make install

	 cmake基本命令格式为：cmake (cmakelist所在目录) (配置)
- LLVM 5.0.0<br><br>
	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所在目录*
<br>
- 开始通过make命令编译<br><br>
   **由于llvm对硬件要求特别高，所以使用`make -j2`来编译**
*此处不使用`make -j4`或`make -j8`因为只给虚拟机分配了3个处理器*<br><br>
   - 多核处理器下提高make的效率
  	  	- `make`:使用单核编译
  	  	- `make -j[n]`:在同一时间并行编译n个任务
  	  	- `make -j`:不限制同一时间并行编译的任务数
  	  	- `make -j2`:一般双核处理器使用
  	  	- `make -j4`:4核处理器
  	  	- 
  	  	<br>
  		*n具体是多少还要根据要编译的项目来定，和处理器个数没有必然关系*		  	<br>		  	<br>
  			*make -j命令并不是任何情况下都可以用的，在存在**编译依赖**的情况       下，单核编译还是一种比较稳妥的方案。*<br><br>
  			
**在`4G内存、3核处理器`下，编译LLVM用时5h**
- 安装 clang 和 llvm
 `make install`<br><br>
 出现 *clang cannot copy /user/local/build/c-text to /user/local/bin*，手动将其复制到/user/local/bin
 <br><br>
 **安装成功**,测试下

[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
import libirpy
File "/home/tianchiliu/hv6/irpy/libirpy/init.py", line 17, in
from ctx import newctx, initctx
File "/home/tianchiliu/hv6/irpy/libirpy/ctx.py", line 18, in
import util
File "/home/tianchiliu/hv6/irpy/libirpy/util.py", line 20, in
import z3
ImportError: No module named z3

-  解决：查看z3 build中的example.py中的内容:
  - 因为4.8版本中没有`bin`目录，要将`bin`改为`build`
  - MYZ3为Z3的安装目录,例如我的完整路径为`/usr/local/z3/build`<br><br>
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
   ```
[参考链接](https://www.cnblogs.com/wainiwann/p/4210343.html)
- 再次`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  设置新的线程数
   ```
     [参考链接](https://stackoverflow.com/questions/344203/maximum-number-of-threads-per-process-in-linux/344292#344292)<br><br>
- `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
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(', ')]<br><br>
修改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
  ```
**成功！**