Skip to content

Instantly share code, notes, and snippets.

View zsrkmyn's full-sized avatar

Stephen Senran Zhang zsrkmyn

85 followers · 39 following
View GitHub Profile
@zsrkmyn
zsrkmyn / declare-datatypes.z3
Created December 26, 2024 15:02
declare-datatypes syntax
; z3 supports two types of syntax for declare-datatypes -- z3's own one and smt-lib 2.6 one
; smt-lib 2.6 syntax
(declare-datatypes (
(Pair 2) ; datatype
)
(
(par (T1 T2) (
(nil) ; constructor 1
(mk-pair (first T1) (second T2)) ; constructor 2
@zsrkmyn
zsrkmyn / bit-masked-and-lower-bound.z3
Created December 25, 2024 10:08
Formal verification for lower bound of bit masked AND
; https://github.com/llvm/llvm-project/pull/120352/
(define-sort I8 () (_ BitVec 8))
(define-fun extract-msb ((x I8)) Int ((_ bv2int 1) ((_ extract 7 7) x)))
(define-fun-rec cl1 ((x I8)) Int (ite (= #x00 x) 0 (ite (= 0 (extract-msb x)) 0 (+ 1 (cl1 (bvshl x #x01))))))
; (assert (= (cl1 #x00) 0))
; (assert (= (cl1 #x01) 0))
; (assert (= (cl1 #x82) 1))
; (assert (= (cl1 #xc1) 2))
; (assert (= (cl1 #xf7) 4))
@zsrkmyn
zsrkmyn / gist:5f74108b15c323242781a2f17f63daaf
Created August 26, 2021 01:16
Reproducer of https://reviews.llvm.org/D107252
typedef unsigned short ushort1024 __attribute__((ext_vector_type(1024)));
typedef unsigned int uint64 __attribute__((ext_vector_type(64)));
// ushort1024 __attribute__((overloadable)) foo(ushort1024 data, uint64 value, uint64 vec_mask){return (ushort1024) (0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0
@zsrkmyn
zsrkmyn / insertPrint.cpp
Created July 23, 2021 07:15
Insert a printf into LLVM IR for debug purpose
static void insertPrint(BasicBlock *BB, StringRef S) {
Module *M = BB->getModule();
LLVMContext &Ctx = M->getContext();
auto *CharPointerTy = PointerType::get(IntegerType::getInt8Ty(Ctx), 0);
auto *PrintfTy =
FunctionType::get(IntegerType::getInt32Ty(Ctx), {CharPointerTy}, true);
auto Printf = M->getOrInsertFunction("printf", PrintfTy);
auto Arr = ConstantDataArray::getString(Ctx, S);
GlobalVariable *GV = new GlobalVariable(
*M, Arr->getType(), true, GlobalValue::PrivateLinkage, Arr, ".str");
@zsrkmyn
zsrkmyn / readfile.c
Created August 22, 2019 08:34
A simple read file function for x86_64 Linux implemented in asm
#include <sys/syscall.h>
#include <stddef.h>
#include <fcntl.h>
int readfile(const char *file, char *buf, size_t size)
{
int ret;
asm (
"mov %[mode], %%rsi \n\t"
"mov %[open], %%rax \n\t"
@zsrkmyn
zsrkmyn / dcl.c
Created June 25, 2019 17:20
dcl
/*
* My 'dcl' implementation of <the C programming language> chap 5.12.
* Slightly different from the given implementation.
*
* Using left recursion elimination to expand 'dirdcl':
* dcl -> optional *'s dirdcl
* dirdcl -> name
* | (dcl)
* | dirdcl()
* | dirdcl[optional size]
@zsrkmyn
zsrkmyn / vibinding.py
Created July 31, 2017 19:45
Dvorak Vi bindings for IPython
# put this file in ~/.ipython/profile_default/startup
# d,h,t,n for move in ViNavigationMode and ViSelectionMode
# jj to kill a line
# jf/F<char> to kill until meeting <char>
from prompt_toolkit.filters.cli import ViNavigationMode, ViSelectionMode, ViMode
from prompt_toolkit.filters import Always, IsReadOnly
from IPython import get_ipython
from prompt_toolkit.key_binding.bindings.vi import create_operator_decorator, create_text_object_decorator, TextObject
from prompt_toolkit.document import Document
from prompt_toolkit.buffer import ClipboardData
@zsrkmyn
zsrkmyn / debian-mips.txt
Created January 19, 2016 10:00
用qemu搭建一个debian-mips环境
1. 下载镜像 https://people.debian.org/~aurel32/qemu/mips{,el}/ ； mips 为大端，mipsel 为小端
2. 设置宿主机网络
```bash
#$ cat network_setup
sudo ip link add qbr0 type bridge
sudo ip addr add 172.20.0.1/16 dev qbr0
sudo ip link set qbr0 up
# sudo dnsmasq -C dnsmasq.conf # for dynamic ip support
```
@zsrkmyn
zsrkmyn / Rvalue_ref.cpp
Last active August 29, 2015 14:20
C++ 学习笔记
#include <iostream>
#include <algorithm>
#include <cstring>
#include <memory>
class MyString {
public:
// Common constructor
MyString(const char * str) :
_len(strlen(str))
@zsrkmyn
zsrkmyn / keybase.md
Created February 3, 2015 17:49
keybase.md

Keybase proof

I hereby claim:

  • I am zsrkmyn on github.
  • I am zsrkmyn (https://keybase.io/zsrkmyn) on keybase.
  • I have a public key whose fingerprint is 0285 FB69 00D1 0203 0550 F20A 3490 8FFB C0BF AC35

To claim this, I am signing this object: