mima.c

#include <assert.h>
#include <stdint.h>
#include <stdbool.h>

/*
OpCode	mnemonik	Description
0	LDC c	c ⟶ Acc
1	LDV a	< a > ⟶ Acc
2	STV a	Acc ⟶ < a >
3	ADD a	Acc + < a > ⟶ Acc
4	AND a	Acc AND < a > ⟶ Acc
5	OR a	Acc OR < a > ⟶ Acc
6	XOR a	Acc XOR < a > ⟶ Acc
7	EQL a	if(Acc == < a >) { -1 ⟶ Acc } else { 0 ⟶ Acc }
8	JMP a	Jump to address a
9	JMN a	Jump to address a if Acc < 0
A	LDIV a	<< a >> ⟶ Acc
B	STIV a	Acc ⟶ << a >>
C	JMS a	jump subroutine
D	JIND a	jump indirect
E		free
F0	HALT	stops the minimal machine
F1	NOT	one's complement(Acc) ⟶ Acc
F2	RAR	rotates Acc on the the right ⟶ Acc
F3 - FF		free
*/

typedef uint8_t opcode;

#define PROGRAM_SIZE 16
#define MEM_SIZE 16
#define MAX_STEPS 16

/* const not working in cbmc
const opcode LDC = 0;
const opcode LDV = 1;
const opcode STV = 2;
const opcode ADD = 3;
const opcode AND = 4;
const opcode OR = 5;
const opcode XOR = 6;
const opcode EQL = 7;
const opcode JMP = 8;
const opcode JMN = 9;
const opcode LDIV = 10;
const opcode STIV = 11;
const opcode JMS = 12;
const opcode JIND = 13;
const opcode FREE = 14;
const opcode HALT = 15;
const opcode NOT = 16;
const opcode RAR = 17;
const opcode NOP = 18;

const opcode UNUSED = 19;
const opcode MAX = 0xF3;
*/

#define LDC 0
#define LDV 1
#define STV 2
#define ADD 3
#define AND 4
#define OR  5
#define XOR 6
#define EQL 7
#define JMP 8
#define JMN 9
#define LDIV 10
#define STIV 11
#define JMS 12
#define JIND 13
#define FREE 14
#define HALT 15
#define NOT 16
#define RAR 17
#define NOP 18

#define UNUSED 19
#define MAX 0xFF

bool is_valid_opcode(opcode op) { return LDC <= op && op < UNUSED; }

/* MIMA MEMORY */
uint16_t program[MAX_STEPS];
uint8_t pc;

int8_t memory[MEM_SIZE];
int8_t acc;


void interpret() {
    for(uint16_t steps = 0; steps < MAX_STEPS; ++steps) {
      __CPROVER_assume(0 <= pc && pc < PROGRAM_SIZE);

      uint16_t word = program[pc];
      opcode op = (word >> 8) & 0xFF;
      uint8_t arg = word & 0xFF;

      __CPROVER_assume(is_valid_opcode(op));

      switch (op) {
      case LDC: // LDC c	c ⟶ Acc
        acc = arg;
        pc++;
        break;
      case LDV: // LDV a	< a > ⟶ Acc
        acc = memory[arg];
        pc++;
        break;
        break;
      case 0x2: // STV a	Acc ⟶ < a >
        memory[arg] = acc;
        pc++;
        break;
      case ADD: // ADD a	Acc + < a > ⟶ Acc
        acc = acc + memory[arg];
        pc++;
        break;
      case AND: // AND a	Acc AND < a > ⟶ Acc
        acc = acc & memory[arg];
        pc++;
        break;
      case OR: // OR a	Acc OR < a > ⟶ Acc
        acc = acc & memory[arg];
        pc++;
        break;
      case XOR: // XOR a	Acc XOR < a > ⟶ Acc
        acc = acc ^ memory[arg];
        pc++;
        break;
      case EQL: // EQL a	if(Acc == < a >) { -1 ⟶ Acc } else { 0 ⟶ Acc }
        if (acc == memory[arg])
          acc = -1;
        else
          acc = 0;
        pc++;
        break;
      case JMP: // JMP a	Jump to address a
        pc = arg;
        break;
      case JMN: // JMN a	Jump to address a if Acc < 0
        if (acc < 0)
          pc = arg;
        else
          pc++;
        break;
      case LDIV: // LDIV a << a >> ⟶ Acc

        // TODO correct effect ?
        // tmp = state.get(arg);
        // throw away bits above address range ...
        // tmp = state.get(tmp & Constants.ADDRESS_MASK);
        // builder.set(State.ACCU, tmp);
        // builder.incIAR();
        acc = memory[memory[arg]];
        pc++;
        break;
      case STIV: // STIV a	Acc ⟶ << a >>
        // TODO Correct effect ?
        memory[memory[arg]] = acc;
        pc++;
        // tmp = state.get(arg);
        // builder.set(tmp & Constants.ADDRESS_MASK, state.get(State.ACCU));
        // builder.incIAR();
        break;
      case JMS: // JMS a	jump subroutine
        // builder.set(arg, state.get(State.IAR) + 1);
        // builder.set(State.IAR, (arg + 1) & Constants.ADDRESS_MASK);
        __CPROVER_assume(false); // TODO Effect is unclear
        pc++;
        break;

      case JIND:                 // JIND a	jump indirect
        __CPROVER_assume(false); // TODO Effect is unclear
        // builder.set(State.IAR, state.get(arg) & Constants.ADDRESS_MASK);
        pc++;
        break;

      case HALT: //	HALT	stops the minimal machine
        return;

      case NOT: // NOT one's complement(Acc) ⟶ Acc
        acc = ~acc;
        pc++;
        break;

      case RAR: // RAR	rotates Acc on the the right ⟶ Acc
        acc = (acc >> 1) | ((acc & 1) << 7);
        pc++;
        break;

      case NOP:
        pc++;
        break;

        // default:
        //   assert(false);
      }
    }
}

int main(void) {
    // for(int i = 0; i < MEM_SIZE; i++) { memory[i] = 0;}
    for(int i = 0; i < PROGRAM_SIZE; i++) { program[i] = nondet_int();}
    acc = 0;
    pc = 0;

    for(int i = 0; i < PROGRAM_SIZE; i++) {
        uint8_t a = nondet_int();
        uint8_t b = nondet_int();
        interpret();
        __CPROVER_assume(memory[0]==a+b);
        //assert(memory[0]==a+b);
    }
    assert(false);
    return 0;
}