Skip to content

Cannot divide 64-bit values in Platin #6

@Emoun

Description

@Emoun

Trying to divide uint64_t will result in Platin complaining there is an unbounded loop.

Example program:

#include <stdio.h> 
#include <stdint.h>
#include <inttypes.h>

uint32_t test_fn (uint32_t x, uint32_t y)  __attribute__ ((noinline));

int main () {
	uint32_t x, y;
	scanf("%" SCNd32 "\n", &x);
	scanf("%" SCNd32 "\n", &y);
	printf("%d\n", (int) test_fn(x, y));
	return 0;
}

uint32_t test_fn (uint32_t x, uint32_t y) {
	return x / y;
}

Trying to analyze the resulting binary for WCET of test_fn will make Platin complain.

Looking into compiler-rt, I see that there is a dedicated function for 32-bit division in the Patmos builtins, but not for 64-bit.
This means the default one is used, which of-course doesn't include loop bounds.

Solution is to implement 64-bit division for Patmos in compile-rt such that it works out of the box.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions