StarGazerM

// #include <cstdio>
// #include <string>
#include <cstdlib>
#include <vector>
#include <algorithm>
#include <cmath>
#include <iostream>
#include <fstream>
#include <chrono>
#include <math.h>

StarGazerM

#include <cmath>
#include <iostream>
#include <chrono>
#include <iomanip>
#include <assert.h>
// #include <thrust/count.h>
#include <thrust/reduce.h>
#include <thrust/unique.h>
#include <thrust/sort.h>

StarGazerM

# escape=`

# Use the latest Windows Server Core 2022 image.
FROM mcr.microsoft.com/windows/servercore:ltsc2022

# Restore the default Windows shell for correct batch processing.
SHELL ["cmd", "/S", "/C"]

RUN `
    # Download the Build Tools bootstrapper.

StarGazerM

//  cclyzer styple fact to value flow graph
// https://llvm.org/docs/LangRef.htm


// edge fact in value flow graph, (directly extracted from llvm IR)

// TODO: need some value type definition here (maybe just operand is enough?)

// access vector/aggregate register `v`, store result in `a`
.decl vector_access(v:symbol, a:symbol)

StarGazerM

Pull docker image

I have a prebuilt one on

docker push stargazermiao/radlog

Run docker image

you can mount your own file to docker container

docker run -it --name radlog -v $(pwd):/workspace stargazermiao/radlog

StarGazerM

method simp(x:int,y:int,z:int, h:bool, hp:bool) returns (l: int, lp: int)
    ensures l == lp
{
  var x1 := x;
  var x2 := x;
  var y1 := y;
  var y2 := y;
  var z1 := z;
  var z2 := z;

StarGazerM

#!/usr/bin/env python3

from typing import Set, List, Iterator
import itertools

import networkx as nx
from networkx.algorithms import bipartite

# YOU WIN NETWORKX FINE. ILL USE YOUR DISGUSTING ALGORITHM.
from networkx.algorithms.matching import max_weight_matching

StarGazerM

#lang racket

;; Assignment 2: Quad-trees and immutable data-structures

(provide total-rect-area)

(define (rect x0 y0 x1 y1)
  `(rect ,(min x0 x1) ,(min y0 y1) ,(max x0 x1) ,(max y0 y1)))

(define (rect-area rect)