vlad902

diff --git a/build.gradle b/build.gradle
index 74ff2a4..3211a21 100644
--- a/build.gradle
+++ b/build.gradle
@@ -24,7 +24,7 @@ allprojects {

 task joernTools(type: Exec) {
     workingDir './python/joern-tools'
-    commandLine 'python3', 'setup.py', 'install', '--user'
+    commandLine 'python3', 'setup.py', 'install'

vlad902

addStep('pp', { verbose=false ->
        delegate.map({
                result = ""
                switch(it.get().class) {
                case com.thinkaurelius.titan.graphdb.vertices.CacheVertex:
                        result = String.format("vertex id: %s\t%s", it.get().id().toString(),
                                it.get().properties().toList().stream()
                                        .filter({ prop -> prop.value() != "" })
                                        .sorted(Comparator.comparing({ prop -> prop.type.toString() }))
                                        .map({ prop -> prop.type.toString() + ": " + prop.value() })

vlad902

// Cute octopus/gremlin query to find all expressions of the form 'foo < 0 ? foo : -foo', these cases are
// likely to not take signed overflow into account, e.g. 0x80000000 (negative signed int max) * -1 = 0x80000000.
g.V().has('type', 'ConditionalExpression')
  .sideEffect { lval = g.V(it.get()).out(AST_EDGE).has('childNum', '1')[0].value('code').replace("- ", "") }
  .filter { lval.matches("[^0-9].*") }
  .sideEffect { rval = g.V(it.get()).out(AST_EDGE).has('childNum', '2')[0].value('code').replace("- ", "") }
  .filter { lval == rval }
  .out(AST_EDGE).has('childNum', '0').astNodes().filter { it.get().value('code') == lval }

vlad902

// Simplify the argument, e.g. '( struct foo* ) & bar' to 'bar'
strip = { traversal ->
	if (traversal.clone().values('type')[0] == 'CastExpression') {
		traversal = traversal.ithChildren('1')
	}

	traversal.values('code')[0].replace("& ", "").replace("* ", "")
}

// { 'aliasing_function': [ 'src_arg', 'dst_arg' ], ... }

vlad902

/**
 * Find code paths that go from a source function to a destination function
 * (only detects direct calls)
 */
allPathsThatCanReach = { srcFunc, dstFunc ->
	__allPathsThatCanReach(srcFunc, dstFunc, [dstFunc])
}

__allPathsThatCanReach = { srcFunc, dstFunc, path ->
	if (srcFunc == dstFunc) {

vlad902

theorem Equation4_implies_by_trivial_rw (G: Type _) [Magma G] (h: Equation4 G) : Equation3 G ∧ Equation8 G ∧ Equation9 G ∧ Equation10 G ∧ Equation11 G ∧ Equation12 G ∧ Equation23 G ∧ Equation24 G ∧ Equation25 G ∧ Equation26 G ∧ Equation27 G ∧ Equation38 G ∧ Equation42 G ∧ Equation47 G ∧ Equation48 G ∧ Equation49 G ∧ Equation50 G ∧ Equation51 G ∧ Equation52 G ∧ Equation53 G ∧ Equation54 G ∧ Equation55 G ∧ Equation56 G ∧ Equation57 G ∧ Equation58 G ∧ Equation59 G ∧ Equation60 G ∧ Equation61 G ∧ Equation99 G ∧ Equation100 G ∧ Equation101 G ∧ Equation102 G ∧ Equation103 G ∧ Equation104 G ∧ Equation105 G ∧ Equation106 G ∧ Equation107 G ∧ Equation108 G ∧ Equation109 G ∧ Equation110 G ∧ Equation111 G ∧ Equation112 G ∧ Equation113 G ∧ Equation151 G ∧ Equation152 G ∧ Equation153 G ∧ Equation154 G ∧ Equation155 G ∧ Equation156 G ∧ Equation157 G ∧ Equation158 G ∧ Equation159 G ∧ Equation160 G ∧ Equation161 G ∧ Equation162 G ∧ Equation163 G ∧ Equation164 G ∧ Equation165 G ∧ Equation203 G ∧ Equation204 G ∧ Equation205 G ∧

vlad902

1,4693,0
10,4630,2788
100,4662,2965
1004,4347,3034
1009,4347,3034
101,4672,2748
1014,4347,3034
102,4645,2985
1020,4692,2394
1021,4564,3000