cbmc: simplify string models a bit, get rid of loops

arekinath · Apr 11, 2024 · 099689a · 099689a
1 parent c29ab6e
commit 099689a
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 17 deletions.
diff --git a/Makefile b/Makefile
@@ -986,10 +986,9 @@ CBMC_AUX=	cbmc-aux.c
 #.piv-apdu.c.cbmc:	CBMC_OPTS+=	--paths lifo
 .piv-apdu.c.cbmc:	CBMC_OPTS+=	--unwind 20
 .piv-apdu.c.cbmc:	CBMC_OPTS+=	--object-bits 12
-.piv-apdu.c.cbmc:	CBMC_OPTS+=	--unwindset tlv_read_string.0:12
 .piv-apdu.c.cbmc:	CBMC_OPTS+=	--unwindset tlv_abort.0:5
-.piv-apdu.c.cbmc:	CBMC_OPTS+=	--unwindset piv_decode_rts.0:10
-.piv-apdu.c.cbmc:	CBMC_OPTS+=	--unwindset piv_decode_rts.1:14
+.piv-apdu.c.cbmc:	CBMC_OPTS+=	--unwindset piv_decode_rts.0:8
+.piv-apdu.c.cbmc:	CBMC_OPTS+=	--unwindset piv_decode_rts.1:8
 
 .tlv.c.cbmc:		CBMC_AUX+=
 .tlv.c.cbmc:		CBMC_OPTS+=	--unwind 10

diff --git a/cbmc-aux.c b/cbmc-aux.c
@@ -788,10 +788,7 @@ tlv_read_upto(struct tlv_state *ts, uint8_t *dest, size_t maxLen,
 		nbytes = maxLen;
 	tc->tc_bytes -= nbytes;
 
-	for (i = 0; i < nbytes; ++i) {
-		uint8_t v;
-		dest[i] = v;
-	}
+	__CPROVER_havoc_slice(dest, nbytes);
 	*len = nbytes;
 
 	return (ERRF_OK);
@@ -824,12 +821,8 @@ tlv_read_string(struct tlv_state *ts, char **dest)
 
 	str = malloc(nbytes + 1);
 	__CPROVER_assume(str != NULL);
-	for (i = 0; i < nbytes; ++i) {
-		char v;
-		__CPROVER_assume(v != 0);
-		str[i] = v;
-	}
-	__CPROVER_assume(str[nbytes] == 0);
+	__CPROVER_assume(__CPROVER_is_zero_string(str));
+	__CPROVER_assume(__CPROVER_zero_string_length(str) == nbytes);
 	*dest = str;
 
 	return (ERRF_OK);
@@ -851,10 +844,7 @@ tlv_read(struct tlv_state *ts, uint8_t *dest, size_t len)
 
 	tc->tc_bytes -= len;
 
-	for (i = 0; i < len; ++i) {
-		uint8_t v;
-		dest[i] = v;
-	}
+	__CPROVER_havoc_slice(dest, len);
 
 	return (ERRF_OK);
 }