sdasgup3 / test-z3.py

Created February 4, 2020 02:03

z3 Solver results affected on the order in which unrelated contraints are added

	import z3
	import sys

	def solve(msg, lvar, xvar, s):
	global status

	s.set("timeout", 60000)
	res = s.check()

	if(z3.unknown == res):

sdasgup3 / vim-plugins.md

Created December 17, 2019 03:56

Plugin management

Instructions

  git clone https://github.com/VundleVim/Vundle.vim.git ~/.vim/bundle/Vundle.vim
  insert the code in .vimrc
  or add more plugins from https://vimawesome.com/
  Launch vim and run :source % and :PluginInstall

Source

sdasgup3 / alltutoroals.md

Last active December 23, 2022 07:53

Few things I am inerested in!

Compiler Tools and Techniques

Compilers

LLVM

sdasgup3 / allProofs.z3

Last active August 26, 2020 06:37

My Z3 proof snippets


	;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
	;;;;;;;;;;;;;;;;;;popcnt expl ;;;;;;;;;;;;;;;;;;;;;;;;;;;
	(declare-const V (_ BitVec 64))
	(declare-const I1 (_ BitVec 64))
	(declare-const I2 (_ BitVec 64))

	(assert
	(not
	(=

sdasgup3 / max_stack_height.cpp

Created May 24, 2018 00:46

Implements a function pass to approximate the max stack height of each McSema lifted function.

	//===-- max_stack_height.cpp - Static analysis for stack height approximation --------------------------------------==//
	//
	// The LLVM Compiler Infrastructure
	//
	// This file is distributed under the University of Illinois Open Source
	// License. See LICENSE.TXT for details.
	//
	//===----------------------------------------------------------------------===//
	//
	// This implements a function pass to approximate the max stack height of each function.

sdasgup3 / stack_deconstructor.cpp

Created May 24, 2018 00:45

Deconstruct the global stack of McSema into local stack frame

	//===-- stack_deconstructor.cpp - Deconstruct the global stack into local stack
	// frame ---===//
	//
	// The LLVM Compiler Infrastructure
	//
	// This file is distributed under the University of Illinois Open Source
	// License. See LICENSE.TXT for details.
	//
	//===----------------------------------------------------------------------===//
	//

sdasgup3 / README.md

Created April 4, 2018 18:36 — forked from hofmannsven/README.md

My simply Git Cheatsheet

Using Git

Global Settings

sdasgup3 / tmux-cheatsheet.markdown

Created November 21, 2017 18:58 — forked from MohamedAlaa/tmux-cheatsheet.markdown

tmux shortcuts & cheatsheet

start new:

tmux

start new with session name:

tmux new -s myname

sdasgup3 / infonum.py

Created November 2, 2017 03:14

Decimal-Hexadecimal-2's complement Binary Calculator

	#!/usr/bin/python

	##############################################################################################################
	# Extract information about a number. #
	# #
	# Example Usage: python infonum.py --bit 4 0xf #
	# Output: #
	# Base 10: -1 #
	# Base 16: f #
	# 2's Compliment binary: 1111 #

sdasgup3 / c++timer.cpp

Created September 10, 2017 01:24

Comparison of various c++ timers

	/* clock example: frequency of primes */
	#include <chrono>
	#include <cstdint>
	#include <math.h> /* sqrt */
	#include <stdio.h> /* printf */
	#include <sys/time.h>
	#include <time.h> /* clock_t, clock, CLOCKS_PER_SEC */

	using namespace std::chrono;

Sandeep Dasgupta sdasgup3