Hi
TaskUse these 2 theorems to prove a theorem:Keywords: pattern matching, goal, tactic, rewriteWhat is goal?goal is the theorem we want to prove in current context, like in this exampleforall p : nat, p × 1 = pintrosfirst, introduce a parameter pCoq automatically match the p with variable in goalrewriterewrite has 2 types: -> and <- for first case you can consider it as expand from LHS(Left Hand Side) to RHS according to the rewrited theorem.p * S O = p * O + p (rewrite theorem mult_n_Sm wit
上图是编译原理课件上的示例，我对前两行实在不解，遂改写为如下版本#include <bits/stdc++.h> using namespace std; int main() { char buf[] = "bababb#"; char* ptr = buf; while (*ptr != '#') { l0: // while (*ptr == 'b') ptr++; // state 0 switch (*ptr) { case 'a': ptr++; goto l1; case 'b': ptr++; goto l0; l1: // while (*ptr == 'a') ptr++; // state 1 switch (*ptr) {
This blog will introduce a BAD PRACTICE, which everyone should avoid.这是一个你可能已经习以为常但可能会导致严重后果的行为--面对大量的变量，不仔细思考各个变量对应的含义是什么，而是直接模仿别的语句的用法直接对照地写。它可能有七八成的概率你的代码可以正常工作，但是这并不是一个好的习惯，一旦产生错误你可能需要付出极大代价。tl;dr先上图。这是我写的一条RISC-V32 addi指令的解析语句，当时写这句的时候好像是快到饭点了，想着快点写完，遂仿照下面那行的格式写，但其实这里的src1已经被计算好是寄存器rs1的值了，所以如此执行，我可能会访问某个编号为uint32_t的寄存器（显然，这很荒谬，因为寄存器成本高，数量肯定有限，访问一个编号为0x12345678的寄存器是不可能的）为什么我第一天没发现呢？因为当时执行的指令是00 00 04 13，rs1的编号为0，rs1存的值也刚好为0，所以没有发生错误。。。。。Appendix引用了(PA)的讲义，值得品读。调试工具与原理在实现监视点的过程中, 你很有可能会碰到段错误.
今天上的嵌入式讲到了ARM的变址寻址，在给出的例子中，立即数均为4，同时老师课上也反复强调ARM是32位的单周期指令，故产生想法：立即数变址寻址是不是必须是4的倍数？带着问题课后和老师讨论完，我感觉这个问题的答案其实挺显然的：肯定不是4的倍数。因为虽然指令是32位 4B的，但是这只能说明存放指令的内存空间是以4B为单位存储的，但是如果要访问存储数据的内存空间，肯定是按字节为单位存放的，这个道理很简单，如果你不管什么变量都以4B为单位，这样会造成极大的空间浪费。
阅读NEMU源码时，发现了没见过的结构体成员声明方式，就是这个":"，问了gpt并STFW了解这个叫做位域指定(Bitfield)。Bitfiled设计的目的应该是用于节省内存空间，比如对于一个开关类型，只需要考虑0和1两种可能，需要的内存只有1b，但是如果你用int存，就会占用16/32位（具体基于平台），如下，gate, b, c三个变量都会存在一个字节里，提升了内存利用率。（虽然在目前的32位机下，整体结构体还是会占4B（可以考虑用printf+sizeof或者gdb调试）struct oneByte { int gate:1; int b:2; int c:6; }; 当然，考虑到内存访问效率，BItField的使用是基于字节对齐的。struct twoBytes { int gate:1; int b:3; int c:6; }; 结构体中第一个字节前四位（@这里说法可能有BUG，考虑到小端法，这个前四位会是低四位还是高四位呢？）被gate和b占用，后面四位为空，c占用第二个字节的六位。Ref:关于位结构体及
Genghong Hu
