require "java"
require "soot-trunk.jar"
require "pry"
require "unific"

#anderes Programm einbinden
require_relative "../lib/test1"

#Ich kopiere das folgende mal und hoffe, dass dann assert funktioniert
require "rubygems"
require "bundler/setup"
require "pp"

#das sollte eigentlich nicht nötig sein, und überschreibt potentiell besseren Code. Problem mit JRuby oder so.
def assert
	if(!yield)
		raise "Fehler in assert."
	end
end
#include "Wrong" löst das Problem. lol. alternativ Wrong.assert{} Warum hat es vorher überhaupt ohne funktioniert? ich check's nicht.

java_import Java::Soot.Main
java_import Java::Soot.toolkits.scalar.BackwardFlowAnalysis
java_import Java::Soot.SceneTransformer
java_import Java::Soot.BodyTransformer
java_import Java::Soot.Scene
java_import Java::Soot.Unit
java_import Java::Soot.SootClass
java_import Java::Soot.toolkits.graph.ExceptionalUnitGraph
#java_import Java::Soot.toolkits.graph.*
java_import Java::Soot.Transform
java_import Java::Soot.PackManager
java_import Java::Soot.toolkits.scalar.ArraySparseSet
java_import Java::Soot.jimple.ReturnStmt
java_import Java::Soot.jimple.ReturnVoidStmt
java_import Java::Soot.jimple.InvokeStmt
java_import Java::Soot.jimple.SpecialInvokeExpr
java_import Java::Soot.jimple.AssignStmt
java_import Java::Soot.jimple.DefinitionStmt
java_import Java::Soot.jimple.IdentityStmt
java_import Java::Soot.jimple.GotoStmt
java_import Java::Soot.jimple.IfStmt
java_import Java::Soot.jimple.EqExpr
java_import Java::Soot.Local
java_import Java::Soot.Value
java_import Java::Soot.RefType
java_import Java::Soot.util.Chain
java_import Java::Soot.jimple.NullConstant
java_import Java::Soot.jimple.internal.JNewExpr
java_import Java::Soot.jimple.internal.JInstanceFieldRef
java_import Java::Soot.SootField

java_import java.util.Iterator

#Um Funktionalität zu erhalten, hier ein paar Funktionen, die nützliche Dinge mit Soot-Objekten tun

def sexp_to_string(sexp_element)
	case sexp_element
		when Array then "[#{sexp_element.map { |x| sexp_to_string(x)}.join(", ")}]"
		when Symbol then ":#{sexp_element.to_s}"
		when Value then  sexp_element.toString() 
		when SootField then sexp_element.toString()
		else raise "???!!!UNBEHANDELTER toString()-Fall:#{sexp_element.class}"
	end
end

def predicate(sexp)
	return sexp[0]
end

def first(sexp)
	return sexp[1][0]
end

def second(sexp)
	return sexp[1][1]
end

#Prüft, wieviele Felder eine Klasse hat, die auf den gleichen Typ zeigen, wie die Klasse selbst ist.
def number_of_same_type_fields(type)
	counter = 0
	if type.is_a? RefType
		sootclass = type.getSootClass()
		fieldchain = sootclass.getFields()
		it = fieldchain.iterator()
		while(it.hasNext()) do
			field = it.next()
			ft = field.getType()
			if type.equals(ft)
				counter += 1
			end
		end
	end
	return counter
end

def cyclic?(type)
	return number_of_same_type_fields(type)>0
end

class MyArraySparseSet < ArraySparseSet
#evtl. mal equivTo überschreiben oder so ähnlich

	#Um Ruby-Syntax zu kriegen, folgendes:
	include Enumerable
	def each(&block)
		it = iterator()
		while(it.hasNext()) do
			aktuelles_element = it.next()
			block.call(aktuelles_element)
		end
	end

	#Um Ruby-Syntax zu kriegen, folgendes:
	def delete_if(&block)
		it = iterator()
		while(it.hasNext()) do
			aktuelles_element = it.next()
			it.remove() if block.call(aktuelles_element)
		end
	end

	#Lösche das Element bei Gleichheit aus dem Set
	def delete(element)
		delete_if{|x| element == x}
	end

	def to_s
		strings = map {|obj| sexp_to_string(obj)}
		str = strings.join(', ')
		return str
	end
end

$merge_counter = 0
$flowthrough_counter = 0

class CyclicityAnalysis < BackwardFlowAnalysis
	def initialize(cfg)
		super(cfg)
		doAnalysis()
	end

	def merge(input1, input2, output)
	$merge_counter += 1
#append_protokoll("Betrete merge(), Anzahl #{$merge_counter}. Input1Inspect=#{input1.inspect} Input1={#{input1}} Input2Inspect=#{input2.inspect} Input2={#{input2}}")
append_protokoll("Betrete merge(), Anzahl #{$merge_counter}. Input1={#{input1}} Input2={#{input2}}")		

		if input1.size() > 3 # Abbruchbedingung, provisorisch um Endlosschleife zu verhindern
		input1.each { |sexp| output.add(deep_copy_sexp(sexp))}
		else
		#Wenn etwas abgeleitet werden kann, lösche es.
			upper = find_ascending_chain_top_element(input2)		
	#		binding.pry if $merge_counter == 31
			if(upper == nil)
				union_soot_sets(input1, input2, output)
			else
				lower = generate_lower_element(upper)
				invariant = generate_invariant(lower)
				union_soot_sets(input1, input2, output)
				output.delete(upper)
				output.delete(lower)
				output.add(invariant)
			end
		#welche Dinge kann man noch ableiten? Das hier läuft auf hässliche quadratisch Suche hinaus. Naja.
append_protokoll("Verlasse merge(). Output=#{output}\n\n") #, outputinspect=#{output.inspect}\n\n")
#append_protokoll("Verlasse merge(). Output=#{output} outputinspect=#{output.inspect}\n\n")		
		end
	end

	def find_ascending_chain_top_element(sexp_set)
		#Durchsuche die neue Menge, finde ein verschachteltes get-Element, gucke, ob das nicht in der alten Menge ist
		sexp_set.each do |sexp|
			if(predicate(sexp)==:noway)
				if(second(sexp).is_a? Array)
					lower = generate_lower_element(sexp)
					if sexp_set.include?(lower)
						return sexp
					end
				end
			end
		end
		return nil
	end

	def generate_lower_element(sexp)
		return [predicate(sexp), [first(sexp), second(sexp)[1]]]
	end

	def generate_invariant(sexp)
		return [:noshare, [first(sexp), second(sexp)]]
	end

	def union_soot_sets(input1, input2, output)
		output.clear()
		input1.each { |sexp| output.add(deep_copy_sexp(sexp))}
		input2.each { |sexp| output.add(deep_copy_sexp(sexp))}
	end

	def copy(source, dest)
	#append_protokoll("enter copy, source=#{source}, sourceinspect=#{source.inspect}, dest=#{dest}, destinspect=#{dest.inspect}")
		dest.clear()
		source.each { |sexp| dest.add(deep_copy_sexp(sexp))}
	#append_protokoll("exit copy, source=#{source}, sourceinspect=#{source.inspect}, dest=#{dest}, destinspect=#{dest.inspect}")
	end
	
	def deep_copy_sexp(sexp)
		if sexp.is_a? Array
			temp_array = []
			sexp.each {|x| temp_array << deep_copy_sexp(x)}
			return temp_array
		else
			return sexp #Symbole und Soot-Objekte werden hier einfach kopiert. Kein deep-copy auf soot-Objekten
		end	
	end

	def flowThrough(input, unit, output)
$flowthrough_counter += 1
#binding.pry if $flowthrough_counter == 250
#append_protokoll("Betrete flowThrough #{$flowthrough_counter}. Input=#{input} Inputinspect=#{input.inspect} Unit:\n#{unit.toString()}")
append_protokoll("Betrete flowThrough #{$flowthrough_counter}. Input=#{input} Unit:\n#{unit.toString()}")		
		case unit
			when IfStmt then flowThrough_if(input, unit, output)
			when GotoStmt then flowThrough_goto(input, unit, output)
			when ReturnStmt, ReturnVoidStmt then flowThrough_return(input, unit, output)
			when IdentityStmt then flowThrough_identity(input, unit, output)
			when InvokeStmt then flowThrough_invoke(input, unit, output)
			when AssignStmt then flowThrough_assign(input, unit, output)
			else raise "Unbehandelter Unit-Fall!" 
		end 
append_protokoll("Verlasse flowThrough. Output=#{output}\n\n")
#append_protokoll("Verlasse flowThrough. Output=#{output} OutputInspect=#{output.inspect}\n\n")	
	end

	def flowThrough_if(input, unit, output)
		copy(input, output)
	end

	def flowThrough_goto(input, unit, output)
		copy(input, output)
	end

	def flowThrough_return(input, unit, output)
		copy(input, output)
	end

	def flowThrough_invoke(input, unit, output)
		if is_constructor(unit)
			flowThrough_invoke_constructor(input, unit, output)
		else
			copy(input, output)
		end
	end

	#kA ob das auch nur ansatzweise richtig implementiert ist. aber bisher macht es noch nix kaputt.
	def is_constructor(unit)
		invoke_expr = unit.getInvokeExpr()
		return invoke_expr.is_a? SpecialInvokeExpr
	end

	#Folgender Fall ist interessant: Wenn der konstruktor von a aufgerufen wird, und :noway, a, x da steht, wird dieses Prädikat erfüllt, außer der Konstruktor macht irgendwelche komischen Sachen. Ich überprüfe den Konstruktor ja selber, das heißt, ich weiß, dass da keine komischen Sachen passieren.
	#Eigentlich muss ich also den Konstruktor noch prüfen, d.h. die Eigenschaften der analysierten Funktion (Konstruktor) hier mit einbeziehen.
	#Ich hab gerade kB mich darum zu kümmern, also tue ich einfach so, als geht beim Aufruf des Konstruktors immer alles glatt.
	#Der Konstruktor heißt init, und wird durch specialinvoke oder so aufgerufen, kA, muss ich noch try-and-error detektiv spielen.
	#wohlbemerkt kann das meistens (immer?) auch weggelassen werden, und im new-statement entfernt werden.dadurch werden die formeln länger mit geschleppt
	def flowThrough_invoke_constructor(input, unit, output)
		copy(input, output)
		invoke_expr = unit.getInvokeExpr()
		neue_variable = get_next_element(invoke_expr) #muss es geben, weil der Konstruktor zu einem Objekt gehören muss.
		output.delete_if {|sexp| noway_element_to_something?(sexp, neue_variable)}
	end

	def noway_element_to_something?(sexp, element)
		if predicate(sexp) == :noway
			if first(sexp) == element
				return true
			end
		end
		return false
	end

	def noway_something_to_element?(sexp, element)
		if predicate(sexp) == :noway
			if second(sexp) == element
				return true
			end
		end
		return false
	end

	def noway_contains_element?(sexp, element)
		if predicate(sexp) == :noway
			if first(sexp) == element || second(sexp) == element
				return true
			end
		end
		return false
	end

	#Identity-Statements sind Zuweisungen von lokalen Parametern durch Stackpositionen, im Jimple-Code mit := und @ bezeichnet. Langweilig.
	def flowThrough_identity(input, unit, output)
		copy(input, output)
	end

	#Regel für Zuweisung:
	#Prüfe (linke Seite oder rechts, ist egal, aber ich nehm mal links.) ob es sich um Knoten-Element handelt. Wenn nicht => Uninteressant. Sonst:
	def flowThrough_assign(input, unit, output)
		left_value_type = unit.getLeftOp().getType()
		if !cyclic?(left_value_type)
			flowThrough_assign_acyclic(input, unit, output)
		else
			flowThrough_assign_cyclic(input, unit, output)			
		end
		cleanup_redundant_sexps(output)
	end

	def cleanup_redundant_sexps(sexp_set)
		if contains?(sexp_set, [:nocycle])
			cleanup_nocycle(sexp_set)
		end
append_protokoll("Vor cleanup redundant noshare: output=#{sexp_set}")
		simplify_noshare(sexp_set)
		delete_noway_redundant_by_noshare(sexp_set)
	end

	def delete_noway_redundant_by_noshare(sexp_set) 
		theorder = lambda{|t1,t2| order(t1, t2)}
		tp = TheoremProver.new($rules, theorder)
		sexp_set.each do |sexp| #Ich glaube, diese Doppelkonstruktion funktioniert nicht, aber ich weiß nicht genau, warum.
			if predicate(sexp) == :noshare
				term_noshare = Set.new
				term_noshare << sexp
				if $flowthrough_counter == 232
					puts sexp_set
					puts sexp_to_string(sexp)
				end
				sexp_set.delete_if do |ziel| 
					erg =  tp.solve(term_noshare, ziel)
					puts "Erg=#{erg}, term_noshare=#{term_noshare}, ziel=#{sexp_to_string(ziel)}"
					next erg
				end
				if $flowthrough_counter == 232
					puts sexp_set
				end
			end
		end
		binding.pry if $flowthrough_counter == 232
	end

#		theorder = lambda{|t1,t2| order(t1, t2)}
#		tp = TheoremProver.new($rules, theorder)
#		term_nocycle = Set.new
#		term_nocycle << [:nocycle]
#		sexp_set.delete_if {|sexp| tp.solve(term_nocycle, sexp)}

	def simplify_noshare(sexp_set)
		result = sexp_set.map do |sexp|
			if predicate(sexp) == :noshare
				next remove_get_from_sexp(sexp)
			else
				next sexp
			end
		end
		sexp_set.clear()
		result.each {|sexp| sexp_set.add(sexp)}
	end

	def remove_get_from_sexp(sexp)
		case predicate(sexp)
			when :nocycle then return sexp
			when :noway then return build_sexp_noway_from_to(remove_all_gets_from_sexp_element(first(sexp)), remove_all_gets_from_sexp_element(second(sexp)))
			when :noshare then return build_sexp_noshare_from_to(remove_all_gets_from_sexp_element(first(sexp)), remove_all_gets_from_sexp_element(second(sexp)))
		end
	end

	def remove_all_gets_from_sexp_element(sexp_element)
		if sexp_element.is_a? Array #aka [:get, a, b]
append_protokoll("Habe get removed")
			return remove_all_gets_from_sexp_element(sexp_element[1])
		else
			return sexp_element
		end
	end

	def contains?(sexp_set, sexp)
		return sexp_set.any? {|e| e == sexp}
	end

	def cleanup_nocycle(sexp_set)
		theorder = lambda{|t1,t2| order(t1, t2)}
		tp = TheoremProver.new($rules, theorder)
		term_nocycle = Set.new
		term_nocycle << [:nocycle]
		sexp_set.delete_if {|sexp| tp.solve(term_nocycle, sexp)}
	end

	def	flowThrough_assign_acyclic(input, unit, output)
		copy(input, output)
	end

	#Unterscheide 3 Fälle:
	#(In allen 3 Fällen die Ersetzungsregel anwenden)
	#0) assign mit new
	#1) x = y
	#2) x.n = y, x Knotentyp
	#3) a.n = y, a kein Knotentyp
	def flowThrough_assign_cyclic(input, unit, output)
		left_value = unit.getLeftOp()
		if assign_element_via_new?(unit)
			flowThrough_assign_cyclic_new(input, unit, output)
		elsif !nested?(left_value)
			flowThrough_assign_cyclic_left_op_not_nested(input, unit, output)
		elsif nested_in_node?(left_value)
			flowThrough_assign_cyclic_left_op_nested_node(input, unit, output)
		else
			flowThrough_assign_cyclic_left_op_nested_neutral(input, unit, output)
		end
	end

	def flowThrough_assign_cyclic_left_op_not_nested(input, unit, output)
			copy(input, output)
			ersetzungsregel_anwenden(output, unit)
			delete_trivially_true_sexps(output)
	end

	def nested_in_node?(left_value)
		next_element = get_next_element(left_value)
		type_of_next_element = next_element.getType()
		return cyclic?(type_of_next_element)
	end

	def flowThrough_assign_cyclic_left_op_nested_neutral(input, unit, output)
			copy(input, output)
			ersetzungsregel_anwenden(output, unit)
	end

	def	flowThrough_assign_cyclic_left_op_nested_node(input, unit, output)
		copy(input, output)
		ersetzungsregel_anwenden(output, unit)
		
		#das hier evtl. ersetzen
		#Hier wird die neue Regel hinzugefuegt (mal auslagern in eigene Funktion!)
		left_value = unit.getLeftOp()
		left_element = get_next_element(left_value)
		left_element_sexp = soot_object_to_sexp(left_element) #Dieser schritt sollte nichts verändern, ist also eigentlich überflüssig
		right_element = unit.getRightOp()
		right_element_sexp = soot_object_to_sexp(right_element)
		neue_sexp = build_sexp_noway_from_to(right_element, left_element)
		output.add(neue_sexp)
	end

	def soot_object_to_sexp(element)
		case element
			when JInstanceFieldRef
				return [:get, element.getBase(), element.getField()]
				#return [:get, element.getBase(), element]
			else
				return element
		end
	end

	def build_sexp_noway_from_to(right_element, left_element)
		return [:noway, [right_element, left_element]]
	end

	def build_sexp_noshare_from_to(right_element, left_element)
		return [:noshare, [right_element, left_element]]
	end

	def assign_element_via_new?(unit)
		right_op = unit.getRightOp()
		return right_op.is_a? JNewExpr
	end

	def flowThrough_assign_cyclic_new(input, unit, output)
			copy(input, output)
			variable = unit.getLeftOp()
			output.delete_if {|sexp| noway_contains_element?(sexp, variable)}
	end

	#Das crasht, wenn es kein nächstes Element gibt.
	def get_next_element(value)
		list_of_elements = value.getUseBoxes()
		list_size = list_of_elements.size()
		next_element_reference = list_of_elements.get(list_size-1)
		next_element = next_element_reference.getValue()
		return next_element
	end

	def get_next_element_box(value)
		list_of_elements = value.getUseBoxes()
		list_size = list_of_elements.size()
		next_element_reference = list_of_elements.get(list_size-1)
		return next_element_reference
	end

	#Der Ausdruck x hat 1 Element. Dagegen hat a.x 2 Elemente, usw.
	def nested?(value)
		value_list = value.getUseBoxes()
		return (value_list.size()!=0)
	end

	def is_object_constructor(unit)
		if unit.is_a? InvokeStmt
			invoke_expr = unit.getInvokeExpr()
			if invoke_expr.is_a? SpecialInvokeExpr
				method = invoke_expr.getMethod()
				method_name = method.getName()
				#method_type = invoke_expr.getType() #ich glaub, das brauch ich hier gar nicht. kA, was ich mir hier original gedacht habe. die ganze Methode ist aber eh weird und durch try&error entstanden weil dokufail.
				if method_name == "<init>"
					return true
				end
			end
		end
	end

	def	delete_trivially_true_sexps(sexp_set)
		sexp_set.delete_if { |x| sexp_trivially_true?(x)}
	end

	def sexp_trivially_true?(sexp)
		#[:noway, [null, x]] mit x!=null ist true. Mit x==null wahrscheinlich auch, aber das behandel ich hier erstmal nicht
		if noway_null_to_something?(sexp)
			return true
		end

		if noshare_contains_null?(sexp)
			return true
		end

		#weitere Fälle hier eintragen
		#[...]

		return false
	end

	def noshare_contains_null?(sexp)
		if predicate(sexp) == :noshare
			if null?(first(sexp)) || null?(second(sexp))
				return true
			end
		end
	end

	#false bei [:noway, null, null]
	def noway_null_to_something?(sexp)
		if(predicate(sexp) == :noway)
			if(null?(first(sexp)) && !null?(second(sexp)))
				return true
			end
		end
		return false
	end

	def null?(value)
		return NullConstant.v.equals(value)
	end

def ersetzungsregel_anwenden(sexp_set, unit)
	left_operator = unit.getLeftOp()
	right_operator = unit.getRightOp()
	new_sexps = sexp_set.map do |sexp|
		next ersetzungsregel(sexp, left_operator, right_operator)
	end
	sexp_set.clear()
	new_sexps.each { |sexp| sexp_set.add(sexp)}
end

def ersetzungsregel(sexp, left_operator, right_operator)
	case predicate(sexp)
		when :noway then ersetze_noway(sexp, left_operator, right_operator)
		when :noshare then ersetze_noshare(sexp, left_operator, right_operator)
		when :nocycle then sexp
		else raise "unbekannte sexp: #{sexp[0]}"
	end
end

def ersetze_noshare(sexp, left_operator, right_operator)
	#Hier benutze ich die Funktionen, die ich zuerst für noway gebaut habe. Möglicherweise kommt hier also totaler Käse raus!
	first_new = ersetze_noshare_sexp_element(first(sexp), left_operator, right_operator)
	second_new= ersetze_noshare_sexp_element(second(sexp), left_operator, right_operator)
	return build_sexp_noshare_from_to(first_new, second_new)
end

def ersetze_noshare_sexp_element(element, left_operator, right_operator)
	if !nested?(left_operator)
		return ersetze_noshare_sexp_element_not_nested(element, left_operator, right_operator)
	else
		return ersetze_noshare_sexp_element_nested(element, left_operator, right_operator)
	end
end

def ersetze_noshare_sexp_element_not_nested(element, left_operator, right_operator)
	#Gehe rekursiv durch element, und ersetze möglichst korrekt
	if element.is_a? Array
		#Es muss sich um ein :get-Ding handeln.
		if element[0] != :get then raise "kein get, oh nein." end
		sub_element = ersetze_noshare_sexp_element_not_nested(element[1], left_operator, right_operator)
		return [:get, sub_element, element[2]] #element[2] muss nicht verändert werden, weil hier nur auf ein Feld zugegriffen wird. Hoffe ich o_O
	else
		if left_operator.equivTo(element)
			return soot_object_to_sexp(right_operator)
		else
			return element
		end
	end
end

def ersetze_noshare_sexp_element_nested(element, left_operator, right_operator)
	if element.is_a? Array
		#Es muss sich um ein :get-Ding handeln.
		if element[0] != :get then raise "kein get, oh nein." end
		#2 Möglichkeiten: entweder geht das Array hier noch tiefer (get-Schachtelung), oder das get ist am Ende.
		#Wenn es am Ende ist, kann man hier vergleichen und evtl. austauschen. Sonst kann man nur tiefer gehen.
		if element[1].is_a? Array
			sub_element = ersetze_noshare_sexp_element_nested(element[1], left_operator, right_operator)
			return [:get, sub_element, element[2]] #hoffentlich muss element[2] wirklich nicht verändert werden, analog zu oben
		else
			left_op_base = get_next_element(left_operator)
			left_op_field = left_operator.getField()
			element_base = element[1]
			element_field = element[2]
			condition_old = (left_op_base.equivTo(element_base) && left_op_field == element_field)
			if condition_old #ähm. lol. historischer überbleibselversuch. achte auf den else-Zweig. (reverse_cf())
				return soot_object_to_sexp(right_operator)
			else
				return element
			end
		end
	else
		#Da der left_operator ein Zugriff auf ein Feld beinhaltet, hier aber nur ein einziges Element steht, können die beiden nicht gleich sein!
		#Ähm, falsch: Für reverse_cf ist genau das nötig.
		left_op_base = get_next_element(left_operator)
		#binding.pry if left_op_base.to_s == "c"
		if left_op_base.equivTo(element)
			return soot_object_to_sexp(right_operator)
		else
			return element
		end
	end
end

def ersetze_noway(sexp, left_operator, right_operator)
	first_new = ersetze_noway_sexp_element(first(sexp), left_operator, right_operator)
	second_new= ersetze_noway_sexp_element(second(sexp), left_operator, right_operator)
	return build_sexp_noway_from_to(first_new, second_new)
	#sexp
end

def ersetze_noway_sexp_element(element, left_operator, right_operator)
	if !nested?(left_operator)
		return ersetze_noway_sexp_element_not_nested(element, left_operator, right_operator)
	else
		return ersetze_noway_sexp_element_nested(element, left_operator, right_operator)
	end
end

def ersetze_noway_sexp_element_not_nested(element, left_operator, right_operator)
	#Gehe rekursiv durch element, und ersetze möglichst korrekt
	if element.is_a? Array
		#Es muss sich um ein :get-Ding handeln.
		if element[0] != :get then raise "kein get, oh nein." end
		sub_element = ersetze_noway_sexp_element_not_nested(element[1], left_operator, right_operator)
		return [:get, sub_element, element[2]] #element[2] muss nicht verändert werden, weil hier nur auf ein Feld zugegriffen wird. Hoffe ich o_O
	else
		if left_operator.equivTo(element)
			return soot_object_to_sexp(right_operator)
		else
			return element
		end
	end
end

def ersetze_noway_sexp_element_nested(element, left_operator, right_operator)
	if element.is_a? Array
		#Es muss sich um ein :get-Ding handeln.
		if element[0] != :get then raise "kein get, oh nein." end
		#2 Möglichkeiten: entweder geht das Array hier noch tiefer (get-Schachtelung), oder das get ist am Ende.
		#Wenn es am Ende ist, kann man hier vergleichen und evtl. austauschen. Sonst kann man nur tiefer gehen.
		if element[1].is_a? Array
			sub_element = ersetze_noway_sexp_element_nested(element[1], left_operator, right_operator)
			return [:get, sub_element, element[2]] #hoffentlich muss element[2] wirklich nicht verändert werden, analog zu oben
		else
			left_op_base = get_next_element(left_operator)
			left_op_field = left_operator.getField()
			element_base = element[1]
			element_field = element[2]
			condition_old = (left_op_base.equivTo(element_base) && left_op_field == element_field)
			if condition_old #ähm. lol. historischer überbleibselversuch. achte auf den else-Zweig. (reverse_cf())
				return soot_object_to_sexp(right_operator)
			else
				return element
			end
		end
	else
		#Da der left_operator ein Zugriff auf ein Feld beinhaltet, hier aber nur ein einziges Element steht, können die beiden nicht gleich sein!
		#Ähm, falsch: Für reverse_cf ist genau das nötig.
		left_op_base = get_next_element(left_operator)
		#binding.pry if left_op_base.to_s == "c"
		if left_op_base.equivTo(element)
			return soot_object_to_sexp(right_operator)
		else
			return element
		end
	end
end

	def replace_sexp_recursively(sexp, &f)
		sexp.each_with_index do |element, index|
			if element.is_a? Array
				replace_sexp_recursively(element, &f)
			else
				sexp[index] = f.call(element)
			end
		end
	end

	def entryInitialFlow
append_protokoll("Betrete entryInitialFlow()")
		a = MyArraySparseSet.new()
		a.add([:nocycle])
append_protokoll("Verlasse entryInitialFlow(). Output=#{a}\n\n")
		return a
	end
	
	def newInitialFlow
		return MyArraySparseSet.new()
	end
end

class Transformer < BodyTransformer
	def initialize
		super()
	end
		
	def internalTransform (body, phaseName, options)
append_protokoll("Betrete internalTransform(). Methode=#{body.getMethod().getName()}")
		cfg = ExceptionalUnitGraph.new(body)
		puts body.toString()
		analyzer = CyclicityAnalysis.new(cfg) #Konstruktor ruft doAnalysis() auf
append_protokoll("Verlasse internalTransform(). Methode=#{body.getMethod().getName()}\n\n")
		puts "internalTransform von " + body.getMethod().getName() + " fertig. Ergebnis:"
		puts body.toString()
		print_ergebnis(cfg, analyzer)
	end

	def print_ergebnis(cfg, analyzer)
		cfg_it = cfg.iterator()
		while(cfg_it.hasNext()) do
			current_unit = cfg_it.next()
			before = analyzer.getFlowBefore(current_unit)
			after = analyzer.getFlowAfter(current_unit)

			puts ""

			print "in: "
			before.each_with_index do |sexp, index|
				print sexp_to_string(sexp)
				print ", " if index < before.size()-1
			end
			print "\n"

			puts current_unit.toString() #kA wieso das nicht crasht

			print "out: "
			after.each_with_index do |sexp, index|
				print sexp_to_string(sexp)
				print ", " if index < after.size()-1
			end
			print "\n"
		end
	end
end

def init_protokoll(dateiname, title)
	$dateiname = dateiname
	open('protokoll', 'w') {|f| f.puts title}
end

def append_protokoll(inhalt)
	open($dateiname, 'a') {|f| f.puts inhalt}
end

#main Start
init_protokoll('protokoll', "BackwardFlowAnalysis")
transformer = Transformer.new
transform = Transform.new("jtp.cyclicityAnalysis", transformer)
PackManager.v().getPack("jtp").add(transform)

puts ARGV
Main.main(ARGV)

#todo für reverse_cf():
#Schritt einfügen: c -> next [c.n=p] p->next einbauen. Achtung: macht eventuell alte Beispiele kaputt! Aber dieser Schritt der analyse ist nötig, sonst kann es nicht funktionieren, denn dieser schritt sorgt für das eigentliche umdrehen der Liste!!!
#2.merge anpassen, um a->c.n, a->c zu a->c zu vereinfachen
