asasMerge branch 'client' of https://code.google.com/p/tcp-learner into client

Adapter/sender.py

@@ -136,6 +136,10 @@ class Sender:
             self.clientIP = packet[IP].src
             # consider adding the parameter: iface="ethx" if you don't receive a response. Also consider increasing the wait time
             scapyResponse = sr1(packet, timeout=self.waitTime, iface=self.networkInterface, verbose=self.isVerbose)
+            if self.useTracking:
+                # the tracker discards retransmits, but scapy doesn't, so don't use scapy
+                scapyResponse = None
+                time.sleep(self.waitTime)
         else:
             time.sleep(self.waitTime)
         captureMethod = ""

Adapter/tracker.py

@@ -67,6 +67,7 @@ class Tracker(threading.Thread):
                 tcp_syn = l3.get_th_seq()
                 tcp_ack = l3.get_th_ack()
                 response = self.impacketResponseParse(l3)
+                # ignore a packet if it was a retransmit
                 if (response.seq, response.ack, response.flags) not in self.responseHistory:
                     if "S" in response.flags:
                         self.responseHistory.add((response.seq, response.ack, response.flags))
@@ -77,7 +78,7 @@ class Tracker(threading.Thread):
     def processResponse(self, response):
         if response is not None:
             self.lastResponse = response
-            if response.flags == "SA" and response in self.lastResponses:
+            if (response.flags == "SA" or response.flags == "AS") and response in self.lastResponses:
                 print 'ignoring SA retransmission ' + response.__str__()
             else:
                 print 'non SA-ret packet:' + response.__str__()

Learner/src/debug/TraceRunner.java

@@ -31,6 +31,8 @@ import util.Log;
 import util.OutputAction;
 
 public class TraceRunner {
+	private static final String PATH = "testtrace.txt";
+	
 	public static final String START = 		"\n****** INPUTS  ******\n";
 	public static final String SEPARATOR = 	"\n****** OUTPUTS ******\n";
 	public static final String END = 		"\n*********************\n";
@@ -44,9 +46,9 @@ public class TraceRunner {
 		Main.handleArgs(args);
 		List<String> trace;
 		try {
-			trace = Files.readAllLines(Paths.get("testtrace.txt"), StandardCharsets.US_ASCII);
+			trace = Files.readAllLines(Paths.get(PATH), StandardCharsets.US_ASCII);
 		} catch (IOException e) {
-			System.out.println("usage of java tracerunner: create a file 'testtrace.txt with the input on each line'");
+			System.out.println("usage of java tracerunner: create a file '" + PATH + "' with the input on each line', optionally preceded by the number of times the input should be repeated");
 			return;
 		}
 		ListIterator<String> it = trace.listIterator();

Learner/src/functionalMappers/TCPMapperSpecification.java

+package functionalMappers;
+
+import sutInterface.Serializer;
+import sutInterface.tcp.Action;
+import sutInterface.tcp.Flag;
+import sutInterface.tcp.FlagSet;
+import sutInterface.tcp.Symbol;
+import sutInterface.tcp.init.ClientInitOracle;
+import sutInterface.tcp.init.FunctionalInitOracle;
+import sutInterface.tcp.init.InitOracle;
+import util.Calculator;
+import util.exceptions.BugException;
+
+/**
+ * Mapper component from abs to conc and conc to abs.
+ * 
+ * @author paul & ramon
+ */
+
+public class TCPMapperSpecification {
+	public static final long NOT_SET = -3; //Integer.MIN_VALUE;
+	public static final long DATA_LENGTH = 4;
+	public static final long WIN_SIZE = 8192;
+
+	/* data variables of the mapper, determined from request/responses */
+	private long lastConcSeqSent, lastConcAckSent, lastConcAckReceived, 
+			lastConcSeqReceived, sutSeq, learnerSeq;
+	private Symbol lastAbsSeqSent;
+	private FlagSet lastFlagsSent, lastFlagsReceived;
+	
+	/*
+	 * boolean state variables, determined from data variables and the current
+	 * values of the boolean variables
+	 */
+	private boolean freshSeqEnabled;
+	private boolean freshAckEnabled;
+	private boolean isLastResponseTimeout;
+	
+	
+	public TCPMapperSpecification() {
+		this( new ClientInitOracle());
+		setDefault();
+		//this( new FunctionalInitOracle());
+		//this( new CachedInitOracle(new InitCacheManager("/home/student/GitHub/tcp-learner/output/1421437324088/cache.txt")));
+	}
+	
+	public TCPMapperSpecification(InitOracle oracle) {
+		//by default, we assume that the start state is the listening state
+		setDefault();
+	}
+	
+	public TCPMapperSpecification clone() {
+		TCPMapperSpecification mapper = new TCPMapperSpecification();
+		mapper.sutSeq = this.sutSeq;
+		mapper.learnerSeq = this.learnerSeq;
+		mapper.lastConcSeqSent = this.lastConcSeqSent;
+		mapper.lastConcAckSent = this.lastConcAckSent;
+		//mapper.lastPacketSent = this.lastPacketSent;
+		//mapper.lastPacketReceived = this.lastPacketReceived;
+		mapper.lastAbsSeqSent = this.lastAbsSeqSent;
+		mapper.lastFlagsReceived = this.lastFlagsReceived;
+		mapper.lastFlagsSent = this.lastFlagsSent;
+		
+		mapper.freshSeqEnabled = this.freshSeqEnabled;
+		mapper.freshAckEnabled = this.freshAckEnabled;
+		return mapper;
+	}
+
+	/* sets all the variables to their default values */
+	public void setDefault() {
+		this.lastConcSeqSent = this.lastConcAckSent = NOT_SET;
+		this.lastConcSeqReceived = this.lastConcAckReceived = NOT_SET;
+		this.sutSeq = this.learnerSeq = NOT_SET;
+		//this.lastPacketSent = new Packet(FlagSet.EMPTY, Symbol.INV, Symbol.INV);
+		//this.lastPacketReceived = new Packet(FlagSet.EMPTY, Symbol.INV, Symbol.INV);			
+		this.lastFlagsReceived = this.lastFlagsSent = FlagSet.EMPTY;
+		this.lastAbsSeqSent = Symbol.INV;
+		this.freshSeqEnabled = true;
+		this.freshAckEnabled = true;
+		this.isLastResponseTimeout = false;
+	}
+
+	/* checks whether the abstractions are defined for the given inputs */
+	/*public boolean isConcretizable(Symbol abstractSeq, Symbol abstractAck) {
+		return !this.freshSeqEnabled || (!Symbol.INV.equals(abstractAck) && !Symbol.INV.equals(abstractSeq));
+	}*/
+	
+	public String processOutgoingRequest(FlagSet flags, Symbol abstractSeq,
+			Symbol abstractAck) {
+		
+		/* check if abstraction is defined */
+		if (this.freshSeqEnabled && (Symbol.INV.equals(abstractAck) || Symbol.INV.equals(abstractSeq))) {
+			return Symbol.UNDEFINED.toString();
+		}
+
+		/* generate input numbers */
+		long concreteSeq;// = getConcrete(abstractSeq, getNextValidSeq());
+		long concreteAck;// = getConcrete(abstractAck, getNextValidAck());
+		if (freshSeqEnabled) {
+			concreteSeq = Calculator.newValue();
+		} else if (abstractSeq == Symbol.V) {
+			concreteSeq = learnerSeq;
+		} else {
+			concreteSeq = Calculator.newOtherThan(learnerSeq);
+		}
+		if (freshAckEnabled) {
+			concreteAck = Calculator.newValue();
+		} else if (abstractAck == Symbol.V) {
+			concreteAck = Calculator.nth(sutSeq, this.lastFlagsReceived.has(Flag.SYN) || this.lastFlagsReceived.has(Flag.FIN) ? 1 : 0);
+		} else {
+			concreteAck = Calculator.newOtherThan(sutSeq);
+		}
+		
+		
+		/* do updates on input */
+		if(this.freshSeqEnabled == true) {
+			this.learnerSeq = concreteSeq;
+		}
+		this.lastConcSeqSent = concreteSeq;
+		this.lastConcAckSent = concreteAck;
+		this.lastFlagsSent = flags;
+		this.lastAbsSeqSent = abstractSeq;
+		
+		/* build concrete input */
+		String concreteInput = Serializer.concreteMessageToString(flags,
+				concreteSeq, concreteAck);
+		return concreteInput;
+	}
+	
+	public String processOutgoingReset() {
+		return (learnerSeq == NOT_SET)? null : Serializer.concreteMessageToString(new FlagSet(Flag.RST), learnerSeq, 0);
+	}
+	
+	public void processOutgoingAction(Action action) {
+		
+	}
+	
+	private long newInvalidWithinWindow(long refNumber) {
+		return Calculator.randWithinRange(Calculator.sum(refNumber, Calculator.MAX_NUM - WIN_SIZE + 2), Calculator.sum(refNumber, Calculator.MAX_NUM/2 + 1));
+	}
+	
+	//modSum(serverSeq, maxNum/2+2), modSum(serverSeq, maxNum - win + 1), modSum(serverSeq, -8191)
+	private long newInvalidOutsideWindow(long refNumber) {
+		return Calculator.randWithinRange(Calculator.sum(refNumber, Calculator.MAX_NUM/2 + 2), Calculator.sum(refNumber, Calculator.MAX_NUM - WIN_SIZE + 1));
+	}
+	/*
+	private long getConcrete(Symbol absToSend, long nextValidNumber) {
+		long nextNumber;
+		switch (absToSend) {
+		case RAND:
+			nextNumber = Calculator.newValue();
+		case V:
+			nextNumber = nextValidNumber;
+			break;
+		case INV:
+			nextNumber = Calculator.newOtherThan(nextValidNumber);
+			break;
+		case IWIN:
+			nextNumber = newInvalidWithinWindow(this.sutSeq);
+			break;
+		case OWIN:
+			nextNumber = newInvalidOutsideWindow(this.sutSeq);
+			break;
+		case WIN:  //not yet tried
+			//nextNumber = Gen.randWithinRange(Gen.sum(1, nextValidNumber), Gen.sum(WIN_SIZE, nextValidNumber));
+			nextNumber = Calculator.randWithinRange(Calculator.sub(nextValidNumber, WIN_SIZE ), Calculator.sub(nextValidNumber, 1));
+			break;
+		default:
+			throw new RuntimeException("Invalid parameter \"" + absToSend
+					+ "\". The input-action used ");
+		}
+		return nextNumber;
+	}*/
+
+	/*private long getNextValidSeq() {
+		long nextSeq;
+		if (this.freshSeqEnabled == true) {
+			nextSeq = Calculator.newValue();
+		} else {
+			nextSeq = this.clientSeq;
+		}
+		return nextSeq;
+	}
+
+	private long getNextValidAck() {
+		long nextAck;
+		if (this.freshAckEnabled == true) {
+			nextAck = Calculator.newValue();
+		} else {
+			nextAck = Calculator.nth(this.serverSeq, this.lastPacketReceived.payload());
+		}
+		return nextAck;
+	}*/
+	
+	public void processIncomingTimeout() {
+		/* state 0 detecting condition */
+		this.isLastResponseTimeout = true;
+		//this.lastPacketReceived = null;
+		checkInit();
+	}
+	
+	public String processIncomingResponse(FlagSet flags, long concreteSeq,
+			long concreteAck) {
+		/* generate output symbols */
+		Symbol abstractSeq = getAbstract(concreteSeq, true);
+		Symbol abstractAck = getAbstract(concreteAck, false);
+		
+		/* do updates on output */
+		if (abstractAck == Symbol.SNCLIENTP1 || abstractAck == Symbol.SNCLIENTPD) {
+			this.learnerSeq = concreteAck;
+		}
+		if (abstractSeq == Symbol.FRESH || abstractSeq == Symbol.SNSERVERP1) {
+			this.sutSeq = concreteSeq;
+		}
+		
+		/* state 0 detecting condition */
+		this.isLastResponseTimeout = false;
+		this.lastConcSeqReceived = concreteSeq;
+		this.lastConcAckReceived = concreteAck;
+		//this.lastPacketReceived = new Packet(flags, abstractSeq, abstractAck);
+		this.lastFlagsReceived = flags;
+		
+		/* build concrete output */
+		String abstractOutput = Serializer.abstractMessageToString(
+				flags, abstractSeq,
+				abstractAck);
+		
+		checkInit();
+		
+		return abstractOutput;
+	}
+
+	private Symbol getAbstract(long nrReceived, boolean isIncomingSeq) {
+		Symbol checkedSymbol;
+		if (nrReceived == Calculator.next(this.learnerSeq)) {
+			checkedSymbol = Symbol.SNCLIENTP1;
+		} else if (nrReceived == Calculator.nth(this.learnerSeq, 2)) {
+			checkedSymbol = Symbol.SNCLIENTP2;
+		} else if (nrReceived == this.learnerSeq) {
+			checkedSymbol = Symbol.SNCLIENT;
+		} else if (nrReceived == this.sutSeq) {
+			checkedSymbol = Symbol.SNSERVER;
+		} else if (nrReceived == Calculator.next(this.sutSeq)) {
+			checkedSymbol = Symbol.SNSERVERP1;
+		} else if (nrReceived == Calculator.nth(this.sutSeq, 2)) {
+			checkedSymbol = Symbol.SNSERVERP2;
+		} else if (nrReceived == this.lastConcSeqSent) {
+			checkedSymbol = Symbol.SNSENT;
+		} else if (nrReceived == this.lastConcAckSent) {
+			checkedSymbol = Symbol.ANSENT;
+		} else if (nrReceived == 0) {
+			checkedSymbol = Symbol.ZERO;
+		} else if (isIncomingSeq == true && this.freshAckEnabled) {
+			checkedSymbol = Symbol.FRESH;
+		} else {
+			checkedSymbol = Symbol.INV;
+		}
+		return checkedSymbol;
+	}
+	
+	protected void checkInit() {
+		boolean sentRST = lastFlagsSent.has(Flag.RST) && this.lastAbsSeqSent.is(Symbol.V);
+		boolean receivedRST = !isLastResponseTimeout && lastFlagsReceived.has(Flag.RST);
+		
+		
+		if (!freshSeqEnabled && (receivedRST || sentRST) || this.lastConcSeqReceived == 0) {
+			freshSeqEnabled = true;
+		} else {
+			freshSeqEnabled = !(lastFlagsSent.has(Flag.SYN)  
+					&& this.lastConcAckReceived == this.lastConcSeqSent + 1)
+					&& freshSeqEnabled;
+		}
+
+		if (receivedRST || sentRST) {
+			freshAckEnabled = true;
+		} else if (lastConcSeqReceived == lastConcAckSent || (!isLastResponseTimeout && lastFlagsReceived.is(Flag.SYN))) {
+			freshAckEnabled = false;
+		}
+	}
+
+	public String getState() {
+		return "MAPPER [FRESH_SEQ=" + this.freshSeqEnabled + "; " +
+				"FRESH_ACK=" + this.freshAckEnabled + "; " +
+				"lastSeqSent=" + this.lastConcSeqSent + 
+				"; lastAckSent=" + this.lastConcAckSent + 
+				"; clientSeq=" + this.learnerSeq + 
+				"; serverSeq=" + this.sutSeq + "]";
+	}
+
+	public String processOutgoingRequest(String flags, String abstractSeq,
+			String abstractAck) {
+
+		/* generate enum classes */
+		Symbol seqSymbol = Symbol.toSymbol(abstractSeq);
+		Symbol ackSymbol = Symbol.toSymbol(abstractAck);
+		FlagSet flagSet = new FlagSet(flags);
+		
+		/* call actual method */
+		String concreteInput = processOutgoingRequest(flagSet, seqSymbol, ackSymbol);
+		return concreteInput;
+	}	
+	
+	public String processIncomingResponse(String flags, long concreteSeq,
+			long concreteAck) {
+		
+		/* generate enum classes */
+		FlagSet flagSet = new FlagSet(flags.toCharArray());
+		
+		/* call actual method */
+		String abstractOutput = processIncomingResponse(flagSet, concreteSeq, concreteAck);
+		return abstractOutput;
+	}
+
+	/* compatibility version */
+	public String processIncomingResponseComp(String flags, String seqReceived,
+			String ackReceived) {
+		long seq = Long.valueOf(seqReceived);
+		long ack = Long.valueOf(ackReceived);
+		String abstractOutput = processIncomingResponse(flags, seq, ack);
+		return abstractOutput;
+	}
+	/*public static void main(String[] args) {
+		TCPMapper mapper = new TCPMapper(null);
+		for (int i = 0; i < 1000; i++) {
+			System.out.println(mapper.newInvalidOutsideWindow(10000));
+			System.out.println(mapper.newInvalidWithinWindow(10000));	
+		}
+	}*/
+	
+	@Override
+	public String toString() {
+		StringBuilder sb = new StringBuilder();
+		sb.append("Mapper state:\n");
+		
+		sb.append("serverSeq: " + sutSeq + "   ");
+		sb.append("clientSeq: " + learnerSeq + "   ");
+//		sb.append("packetSent: " + lastPacketSent + "   ");
+//		sb.append("packetRecv: " + lastPacketReceived + "   ");
+//		sb.append("lastSeqSent: " + lastSeqSent + "   ");
+//		sb.append("lastAckSent: " + lastAckSent + "   ");
+//		sb.append("dataAcked: " + dataAcked + "   ");
+//		sb.append("lastFlagsSent: " + lastFlagsSent + "   ");
+//		sb.append("lastFlagsReceived: " + lastFlagsReceived + "   ");
+//		sb.append("lastAbstractSeqSent: " + lastAbstractSeqSent + "   ");
+//		sb.append("lastAbstractAckSent: " + lastAbstractAckSent + "   ");
+//		sb.append("lastAbstractSeqReceived: " + lastAbstractSeqReceived + "   ");
+//		sb.append("lastAbstractAckReceived: " + lastAbstractAckReceived + "   ");
+		sb.append("isInit: " + freshSeqEnabled + "   ");
+		sb.append("isLastResponseTimeout: " + isLastResponseTimeout + "   ");
+		/*
+		 * boolean state variables, determined from data variables and the current
+		 * values of the boolean variables
+		 */
+		return sb.toString();
+	}
+}

Learner/src/functionalMappers/TCPSutWrapperSpecification.java

+package functionalMappers;
+
+import java.util.HashMap;
+import java.util.Map;
+
+import sutInterface.SocketWrapper;
+import sutInterface.SutWrapper;
+import sutInterface.tcp.Action;
+import sutInterface.tcp.Internal;
+import sutInterface.tcp.Symbol;
+import util.InputAction;
+import util.Log;
+import util.OutputAction;
+
+// SutWrapper used for learning TCP (uses abstraction) 
+// Unlike SimpleSutWrapper, all communication is directed through a mapper component
+public class TCPSutWrapperSpecification implements SutWrapper{
+
+	private final static Map<Integer,SocketWrapper> socketWrapperMap = new HashMap<Integer, SocketWrapper>();
+	private TCPMapperSpecification mapper;
+	private TCPMapperSpecification previousMapper;
+	private final SocketWrapper socketWrapper;
+	
+	public TCPSutWrapperSpecification(int tcpServerPort, TCPMapperSpecification mapper) {
+		this(tcpServerPort);
+		this.mapper = mapper;
+	}
+	
+	public TCPSutWrapperSpecification(int tcpServerPort) {
+		if(socketWrapperMap.containsKey(tcpServerPort)) {
+			this.socketWrapper = socketWrapperMap.get(tcpServerPort); 
+		} else {
+			this.socketWrapper = new SocketWrapper(tcpServerPort);
+			socketWrapperMap.put(tcpServerPort,this.socketWrapper);
+			Runtime.getRuntime().addShutdownHook(new Thread() {
+				public void run() {
+					Log.fatal("Detected shutdown, commencing connection "+ 
+							socketWrapper + " termination");
+					if (socketWrapper != null) {
+						try {
+							Log.fatal("Sending an exit message to the adapter");
+							socketWrapper.writeInput("exit");
+						} finally {
+							Log.fatal("Closing the socket");
+							socketWrapper.close();
+						}
+					}
+				}
+			});
+		}
+		
+	}
+	
+	public TCPSutWrapperSpecification(int tcpServerPort, TCPMapperSpecification mapper, boolean exitIfInvalid) {
+		this(tcpServerPort, mapper);
+	}
+	
+	private static TCPSutWrapperSpecification tcpWrapper = null;
+	public static void setTCPSutWrapper(TCPSutWrapperSpecification tcpWrapper) {
+		TCPSutWrapperSpecification.tcpWrapper  = tcpWrapper;
+	}
+	public static TCPSutWrapperSpecification getTCPSutWrapper() {
+		return TCPSutWrapperSpecification.tcpWrapper;
+	}
+	
+	public OutputAction sendInput(InputAction symbolicInput) {
+		OutputAction symbolicOutput;
+		previousMapper = mapper.clone();
+		
+		// Build concrete input
+		String abstractRequest = symbolicInput.getValuesAsString(); 
+		String concreteRequest;
+		
+		// Internal inputs are handled first. They have no effect on the system
+		if(Internal.isInternalCommand(abstractRequest)) {
+			if(Internal.valueOf(abstractRequest) == Internal.REVERT) {
+				mapper = previousMapper;
+				sendReset();
+				return null;
+			} 
+		}
+
+		
+		Log.info("MAPPER BEFORE:" + mapper.getState());
+		// processing of action-commands
+		// note: mapper is not updated with action commands
+		
+		if(Action.isAction(abstractRequest)) {
+			this.mapper.processOutgoingAction(Action.valueOf(abstractRequest));
+			concreteRequest = abstractRequest.toLowerCase();
+		}
+		// only processing of packet-requests
+		else {
+			concreteRequest = processOutgoingPacket(abstractRequest);
+		}
+
+		Log.info("MAPPER INTER:" + mapper.getState());
+		
+		// Handle non-concretizable abstract input case
+		if(concreteRequest.equalsIgnoreCase(Symbol.UNDEFINED.name())) {
+			symbolicOutput = new OutputAction(Symbol.UNDEFINED.name());
+		}
+		// Send concrete input, receive output from SUT and make abs
+		else {
+			String concreteResponse = sendPacket(concreteRequest);
+			String abstractResponse = processIncomingPacket(concreteResponse);
+			symbolicOutput = new OutputAction(abstractResponse);
+		}
+		Log.info("MAPPER AFTER:" + mapper.getState());
+		
+		return symbolicOutput;
+	}
+
+	
+	/**
+	 * called by the learner to reset the automaton
+	 */
+	public void sendReset() {
+		Log.info("******** RESET ********");
+		String rstMessage = mapper.processOutgoingReset();
+		// mapper made a pertinent reset message
+		if(rstMessage != null) {
+			socketWrapper.writeInput(rstMessage);
+			socketWrapper.readOutput();
+		}
+		socketWrapper.writeInput("reset");
+		mapper.setDefault();
+	}
+	
+	/**
+	 * Updates seqToSend and ackToSend correspondingly.
+	 * 
+	 * @param abstract input e.g. "FA(V,INV)"
+	 * @return concrete output of the form "flags seqNr ackNr" describing a
+	 *         packet, e.g. "FA 651 814", through the socket.
+	 */
+	private String processOutgoingPacket(String input) {
+		String[] inputValues = input.split("\\(|,|\\)"); // of form {flags, seq,
+															// ack}, e.g.
+															// {"FIN+ACK", "V",
+															// "INV"}
+		String flags = inputValues[0];
+		String abstractSeq = inputValues[1];
+		String abstractAck = inputValues[2];
+
+		String concreteInput = mapper.processOutgoingRequest(flags,
+				abstractSeq, abstractAck);
+		return concreteInput;
+	}
+
+	private String sendPacket(String concreteRequest) {
+		if (concreteRequest == null) {
+			socketWrapper.writeInput("nil");
+		} else {
+			socketWrapper.writeInput(concreteRequest);
+		}
+		String concreteResponse = socketWrapper.readOutput();
+		return concreteResponse;
+	}
+	
+	/**
+	 * 
+	 * @param concreteResponse 
+	 *            of the form "flags seqNr ackNr", e.g. "FA 1000 2000"
+	 * @return output, e.g. "FA(V,INV)"
+	 */
+	private String processIncomingPacket(String concreteResponse) {
+		String abstractResponse;
+		if (concreteResponse.equals("timeout")) {
+			mapper.processIncomingTimeout();
+			abstractResponse = "TIMEOUT";
+		} else {
+			String[] inputValues = concreteResponse.split(" ");
+			String flags = inputValues[0];
+
+			long seqReceived = Long.parseLong(inputValues[1]);
+			long ackReceived = Long.parseLong(inputValues[2]);
+			abstractResponse = mapper.processIncomingResponse(flags,
+					seqReceived, ackReceived);
+		}
+		return abstractResponse;
+	}