search

herd / herdtools7

The Herd toolsuite to deal with .cat memory models (version 7.xx)
Other
228 stars 65 forks source link

Herdtools does not build on 32-bit systems #154

Closed eth-arm closed 3 years ago

eth-arm commented 3 years ago

Trying to build herdtools7 on a Raspberry Pi running Raspbian Buster 32-bit fails with:

% make
sh ./dune-build.sh $HOME
+ ./version-gen.sh /home/eth
+ dune build --profile release @all
File "lib/symbConstant.ml", line 37, characters 45-56:
Error: Integer literal exceeds the range of representable integers of type int
File "lib/symbValue.ml", line 115, characters 21-32:
Error: Integer literal exceeds the range of representable integers of type int
make: *** [Makefile:32: build] Error 1

This seems to be because the size of int is dependent on machine architecture, and the bit-manipulation in symbConstant.ml assumes a 64-bit architecture.

maranget commented 3 years ago

You are correct, if port to 32 bits is considered important, one may consider implementing the 'cap' field as int64. However, I am wondering what is the minimal size required for this field?

eth-arm commented 3 years ago

After asking @ambroise-arm, the Capability is bits 128 to 95 of a 129-bit register, which does not fit into an Int32, so I think it should be Int64.

maranget commented 3 years ago

Ok thanks, good to know.

maranget commented 3 years ago

The issue is hopefully closed by PR #179, which implements Morello capacities as OCaml int64 type.