Bounded model checking with CBMC and Glucose

December 10, 2020 · Un minuto· Tags:Bmc, C, Cbmc, Glucose, Sat

Ho pubblicato un nuovo post (in inglese) dal titolo “Bounded model checking with CBMC and Glucose”.

C: Packing di due interi in un'unica variabile

January 11, 2018 · Un minuto· Tags:C

Di recente avevamo bisogno di usare un’unica variabile int per contenere due interi di piccole dimensioni. (Lasciamo perdere i dettagli e facciamo finta che int sia una variabile a 32 bit, ok?) Nulla di complicato, ma comunque ci sono voluti un paio di tentativi prima che tutto filasse liscio. Quindi, se a qualcuno servisse, ecco il codice:

	#include "stdio.h"
	#include "stdlib.h"
	#define W 15 // Bit-Width of tuple elements (Up to 15 is fine)

	const int MASK = (1U << W) - 1;
	const int MASK2W = (1U << 2*W) - 1;
	const int m = 1U << (W - 1);

	/**
	* @brief Trim n into bit-width W.
	* @return A two's complmenent, W-bit representation of n.
	*/
	inline int trim(int n) {
	n = n >= 0 ? abs(n) : ~abs(n) + 1;
	return n & MASK;
	}

	/**
	* @brief Extend the sign of x
	* @details see: https://graphics.stanford.edu/~seander/bithacks.html#VariableSignExtend
	* @param x A two's complement, W-bit representation of an integer
	* @return an int containing the same integer represented by x
	*/
	inline int signExtend(int x) {
	return ((x & MASK) ^ m) - m;
	}


	/**
	* @brief Pack x and y into a tuple.
	*/
	int packTuple(int x, int y) {
	int tup = trim(y) \| (trim(x) << W);
	tup &= MASK2W;
	return tup;
	}

	int getX(int tup) {
	return signExtend(tup >> W);
	}

	int getY(int tup) {
	return signExtend(tup);
	}

	/**
	* @brief Check that a tuple has been packed correctly
	* @details [long description]
	*
	* @param tup The tuple to check
	* @param expectedX Expected first element of the tuple
	* @param expectedY Expected second element of the tuple
	* @return 1 if tup == (expectedX, expectedY); 0 otherwise
	*/
	int testTuple(int tup, int expectedX, int expectedY) {
	return (expectedX == getX(tup) && expectedY == getY(tup));
	}


	void printTuple(int tup) {
	int x = getX(tup);
	int y = getY(tup);
	printf("t: %x (x: %i, y:%i)\n", tup, x, y);
	}

	/**
	* @brief Returns the elemwnt-wise sum of two tuples
	* @return The tuple `(t1.x + t2.x, t1.y + t2.y)`
	*/
	int sum(int t1, int t2) {
	return packTuple(getX(t1)+getX(t2), getY(t1)+getY(t2));
	}

	/**
	* @brief Test that everything works
	* @details This will test that all possible tuples are correctly packed and
	* unpacked. If something goes wrong, it will print some data about the tuple
	* that failed to unpack.
	*/
	int main(void) {
	const int MAXELEM = (1U << (W-1));

	for(int x = -MAXELEM+1; x < MAXELEM; ++x) {
	for(int y = -MAXELEM+1; y < MAXELEM; ++y) {
	int t = packTuple(x, y);
	if (!testTuple(t, x, y)) {
	printf("ERROR x: %i, y: %i\n", x, y);
	printTuple(t);
	return 1;
	}
	}
	// printf("%i\n", x);
	}

	return 0;
	}

view raw tuple.c hosted with ❤ by GitHub

Il main() proverà tutte le possibili coppie, terminando con un errore se l’unpacking di una tupla porta a risultati inattesi.

Continua »