Add static analysis to CI

.github/workflows/ci.yaml

@@ -13,10 +13,10 @@ jobs:
   ci:
     runs-on: ubuntu-latest
     container:
-      image: ghcr.io/tillitis/tkey-builder:3
+      image: ghcr.io/tillitis/tkey-builder:4
     steps:
       - name: checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           # fetch-depth: 0
           persist-credentials: false
@@ -26,6 +26,21 @@ jobs:
         run: |
           git config --global --add safe.directory "$GITHUB_WORKSPACE"
 
+      - name: check indentation of our firmware C code
+        working-directory: hw/application_fpga
+        run: |
+          make -C fw/tk1 checkfmt
+          make -C fw/testfw checkfmt
+
+      - name: run static analysis on firmware C code
+        working-directory: hw/application_fpga
+        run: |
+          make check
+
+      - name: lint verilog using verilator
+        working-directory: hw/application_fpga
+        run: make lint
+
       - name: compile ch552 firmware
         working-directory: hw/boards/mta1-usb-v1/ch552_fw
         run: make
@@ -38,16 +53,6 @@ jobs:
         working-directory: hw/application_fpga
         run: make firmware.bin testfw.bin
 
-      - name: check fmt of our firmware C code
-        working-directory: hw/application_fpga
-        run: |
-          make -C fw/tk1 checkfmt
-          make -C fw/testfw checkfmt
-
-      - name: lint verilog using verilator
-        working-directory: hw/application_fpga
-        run: make lint
-
       # doing this last as it takes long time
       - name: make application FPGA gateware
         working-directory: hw/application_fpga

contrib/Dockerfile

@@ -42,7 +42,7 @@ RUN apt-get -qq update -y \
                vim \
                xdot \
                sdcc \
-               splint \               
+               splint \
                cmake \
                gcc-arm-none-eabi \
                libnewlib-arm-none-eabi \

contrib/Makefile

@@ -5,7 +5,7 @@
 BUILDIMAGE=tkey-builder-local
 
 # default image used when running a container
-IMAGE=ghcr.io/tillitis/tkey-builder:3
+IMAGE=ghcr.io/tillitis/tkey-builder:4
 
 all:
 	@echo "Targets:"

hw/application_fpga/Makefile

@@ -149,6 +149,9 @@ firmware.elf: $(FIRMWARE_OBJS) $(P)/fw/tk1/firmware.lds
 .PHONY: check
 check:
 	clang-tidy -header-filter=.* -checks=cert-* $(FIRMWARE_SOURCES) -- $(CFLAGS)
+
+.PHONY: splint
+splint:
 	splint -nolib -predboolint +boolint -nullpass -unrecog -infloops -initallelements -type -unreachable -unqualifiedtrans -fullinitblock $(FIRMWARE_SOURCES)
 
 testfw.elf: $(TESTFW_OBJS) $(P)/fw/tk1/firmware.lds
@@ -165,6 +168,8 @@ testfw.hex: testfw.bin testfw_size_mismatch
 
 .PHONY: check-binary-hashes
 check-binary-hashes:
+	sha512sum firmware.bin
+	sha256sum application_fpga.bin
 	sha512sum -c firmware.bin.sha512
 	sha256sum -c application_fpga.bin.sha256
 
@@ -350,6 +355,8 @@ help:
 	@echo "Supported targets:"
 	@echo "------------------"
 	@echo "all                Build all targets."
+	@echo "check              Run static analysis on firmware."
+	@echo "splint             Run splint static analysis on firmware."
 	@echo "firmware.elf       Build firmware ELF file."
 	@echo "firmware.hex       Build firmware converted to hex, to be included in bitstream."
 	@echo "bram_fw.hex        Build a fake BRAM file that will be filled in later after place-n-route."

hw/application_fpga/application_fpga.bin.sha256

@@ -1 +1 @@
-27a17eed9376111f5beb92d3c2c58dacca975a54534d05c25a92c5573920c291  application_fpga.bin
+5b373c0ab86b8970b28270bb54825e1dc7f9723a80598ad85851c2b3aabed989  application_fpga.bin

hw/application_fpga/firmware.bin.sha512

@@ -1 +1 @@
-f53d7d86f92b796d750995c6540843b53346b58c4b97a57a290f6ae799e50d7e7afad519aa37277c17d476417d5a7d45f840dd2ed6ede3564602ff75c9007488  firmware.bin
+e28f9f103e4f027ff9f137f94eef4218a486bd2b518a847b5ff7ccaa7eaf8308c07864d03d54dedcf9866e895fc119687381a6dd8f5d2f013b6a6d0437251f76  firmware.bin

hw/application_fpga/fw/tk1/assert.c

@@ -20,8 +20,10 @@ void assert_fail(const char *assertion, const char *file, unsigned int line,
 	htif_puts(function);
 	htif_lf();
 
+#ifndef S_SPLINT_S
 	// Force illegal instruction to halt CPU
 	asm volatile("unimp");
+#endif
 
 	// Not reached
 	__builtin_unreachable();

hw/application_fpga/fw/tk1/lib.c

@@ -104,6 +104,7 @@ void *memset(void *dest, int c, unsigned n)
 	for (; n; n--, s++)
 		*s = (uint8_t)c;
 
+	/*@ -temptrans @*/
 	return dest;
 }
 
@@ -117,6 +118,11 @@ void memcpy_s(void *dest, size_t destsize, const void *src, size_t n)
 	uint8_t *dest_byte = (uint8_t *)dest;
 
 	for (size_t i = 0; i < n; i++) {
+		/*@ -nullderef @*/
+		/* splint complains that dest_byte and src_byte can be
+		 * NULL, but it seems it doesn't understand assert.
+		 * See above.
+		 */
 		dest_byte[i] = src_byte[i];
 	}
 }

hw/application_fpga/fw/tk1/main.c

@@ -92,8 +92,8 @@ static uint32_t rnd_word(void)
 static void compute_cdi(const uint8_t *digest, const uint8_t use_uss,
 			const uint8_t *uss)
 {
-	uint32_t local_uds[8];
-	uint32_t local_cdi[8];
+	uint32_t local_uds[8] = {0};
+	uint32_t local_cdi[8] = {0};
 	blake2s_ctx secure_ctx = {0};
 	uint32_t rnd_sleep = 0;
 	int blake2err = 0;
@@ -115,7 +115,7 @@ static void compute_cdi(const uint8_t *digest, const uint8_t use_uss,
 	// while on the firmware stack which is in the special fw_ram.
 	wordcpy_s(local_uds, 8, (void *)uds, 8);
 	blake2s_update(&secure_ctx, (const void *)local_uds, 32);
-	memset(local_uds, 0, 32);
+	(void)memset(local_uds, 0, 32);
 
 	// Update with TKey program digest
 	blake2s_update(&secure_ctx, digest, 32);
@@ -268,7 +268,9 @@ static enum state loading_commands(const struct frame_header *hdr,
 			nbytes = ctx->left;
 		}
 		memcpy_s(ctx->loadaddr, ctx->left, cmd + 1, nbytes);
+		/*@-mustfreeonly@*/
 		ctx->loadaddr += nbytes;
+		/*@+mustfreeonly@*/
 		ctx->left -= nbytes;
 
 		if (ctx->left == 0) {
@@ -396,7 +398,12 @@ int main(void)
 	// Let the app know the function adddress for blake2s()
 	*fw_blake2s_addr = (uint32_t)blake2s;
 
+	/*@-mustfreeonly@*/
+	/* Yes, splint, this points directly to RAM and we don't care
+	 * about freeing anything was pointing to 0x0 before.
+	 */
 	ctx.loadaddr = (uint8_t *)TK1_RAM_BASE;
+	/*@+mustfreeonly@*/
 	ctx.use_uss = FALSE;
 
 	scramble_ram();
@@ -436,5 +443,7 @@ int main(void)
 		}
 	}
 
+	/*@ -compdestroy @*/
+	/* We don't care about memory leaks here. */
 	return (int)0xcafebabe;
 }

hw/application_fpga/fw/tk1/proto.c

@@ -167,7 +167,7 @@ static int read(uint8_t *buf, size_t bufsize, size_t nbytes)
 // bytelen returns the number of bytes a cmdlen takes
 static int bytelen(enum cmdlen cmdlen)
 {
-	int len;
+	int len = 0;
 
 	switch (cmdlen) {
 	case LEN_1:

hw/application_fpga/fw/tk1/proto.h

@@ -50,6 +50,7 @@ struct frame_header {
 	enum cmdlen len;
 };
 
+/*@ -exportlocal @*/
 void writebyte(uint8_t b);
 uint8_t readbyte(void);
 void fwreply(struct frame_header hdr, enum fwcmd rspcode, uint8_t *buf);