Addition to proof of correctness

This commit is contained in:
Yannick Reiß 2023-10-04 10:06:58 +02:00
parent ba7f2d8394
commit 8da2a2b27e
No known key found for this signature in database
GPG Key ID: 5A3AF456F0A0338C
2 changed files with 144 additions and 1 deletions

View File

@ -82,4 +82,65 @@ are implemented memory safe.
## Every program, which is accepted by the compiler without error is working on the processor.
The 8 operators of brainfuck can be divided into two different groups:
- < > + - , .
- [ ]
The operators of the first group can be used
- in any order
- with any amount
Following those conditions, there is no need for a syntax check, as every order is a valid program.
This is different with the second group, which holds the loop operators.
Those need to
- be included in a certain order: [ ]
- be included in the code with the same amount: $w_[ = w_]$
The code must be checked for the right amount and order of loop operators.
This is done by using the following code:
```c
for (char* cursor = token; *cursor; cursor++) {
/* Analyze form */
if (*cursor == '[') {
rv += 1;
} else if (*cursor == ']') {
rv -= 1;
}
/* Check value for errors. */
if (rv < 0) {
(void)printf("ERROR!\n");
rv = EXIT_FAILURE;
break;
}
/* check for nested loops */
if (rv > 1) {
(void)printf("WARNING!\n");
}
}
if (rv > 0) {
(void)printf("ERROR!\n");
rv = EXIT_FAILURE;
}
```
The value of rv is checked for the following conditions:
|Condition|Reaction|Description|
|---------|--------|-----------|
| $<0$ |ERROR |A closing bracket is ending a non-existing loop. There is no address to jump back to.|
| $>2$ |WARNING |A nested bracket is opened. Although this is not wrong for brainfuck, my circuit does currently not support this.|
| $>0$ |ERROR |This is checked after the loop. If the value of rv is greater than zero, a bracket was not closed.|
The last check maybe could be handled as warning, because the program can be run in a loop, even if it would never end.
By doing this check on the given program, it's safe to assume, that every program, that is accepted by the compiler, can be run.
## The compiled binaries are working the same way as the provided code.

View File

@ -74,6 +74,86 @@ static char* intoLogisim (char* tokens) {
return binary;
}
/**
* @name intoC
* @return static char*
* @brief Return binary as c file.
*
* @param char* tokens
*/
static char* intoC (char* tokens) {
return 0;
char* binary = 0;
/* TODO: Change size to match C language */
/* Using c with the current memory space (256x4) has the fixed size of 533 bytes. */
int filesize = 533;
int pos = 0; /* used to navigate around binary */
/* Allocate memory for binary */
binary = (char*)malloc(sizeof(char) * filesize);
if (!binary) {
/* Error */
perror("malloc error on memory allocation of: binary");
exit(EXIT_FAILURE);
}
/* TODO: Replace by C program */
char version_number[] = "v3.0 hex words plain";
for (int i = 0; i < 20; i++) {
binary[i] = version_number[i];
}
pos = 20; /* position after loop */
binary[pos++] = '\n';
int pos_space = pos + 1; /* save the index to fill with spaces here */
/* Loop through tokens and add matching code to binary. */
for (char* cursor = tokens; *cursor; cursor++) {
/* TODO: Replace by C thingies */
/* Switch case holds all operands. */
switch (*cursor) {
case '>': binary[pos] = '0';break;
case '<': binary[pos] = '1';break;
case '+': binary[pos] = '2';break;
case '-': binary[pos] = '3';break;
case ',': binary[pos] = '4';break;
case '.': binary[pos] = '5';break;
case '[': binary[pos] = '6';break;
case ']': binary[pos] = '7';break;
default: return (char*)EXIT_FAILURE;
}
/* every second position is space or newline */
pos += 2;
}
/* fill remaining instruction space with > operations */
for (; pos < filesize; pos += 2) {
binary[pos] = '0';
}
/* reset position to the first space and start filling up */
pos = pos_space;
for (; pos < filesize; pos += 2) {
/* Calculate whether to use space or newline. */
if ((pos - 20) % 64 == 0) {
binary[pos] = '\n';
} else {
binary[pos] = ' ';
}
}
/* Finally, end the string. */
binary[filesize-1] = '\n';
return binary;
}
/**
* @name assemble
* @return char*
@ -88,7 +168,9 @@ char* assemble (char* device, char* tokens) {
/* supported devices are hardcoded here. */
if (!strcmp(device, "logisim")) {
rv = intoLogisim(tokens);
} else {
} else if (!strcmp(device, "c")) {
rv = intoClang(tokens);
}else {
(void)printf("ERROR: Chosen device %s does not exist!\n", device);
rv = (char*)EXIT_FAILURE;
}