clang-format

.clang-format

@@ -0,0 +1,141 @@
+---
+AccessModifierOffset: -4
+AlignAfterOpenBracket: Align
+AlignArrayOfStructures: None
+
+# dont align consecutive things, otherwise git diffs are painful
+AlignConsecutiveAssignments: false
+AlignConsecutiveBitFields: false
+AlignConsecutiveDeclarations: false
+AlignConsecutiveMacros: false
+AlignEscapedNewlines: DontAlign
+AlignOperands: true
+AlignTrailingComments: false
+SpacesBeforeTrailingComments: 1
+
+# line breaking/reflow
+# .. preserve block-indented args/params
+AllowAllArgumentsOnNextLine: true
+AllowAllParametersOfDeclarationOnNextLine: true
+#
+AllowShortEnumsOnASingleLine: false
+AllowShortBlocksOnASingleLine: false
+AllowShortCaseLabelsOnASingleLine: false
+AllowShortFunctionsOnASingleLine: false
+AllowShortLambdasOnASingleLine: false
+AllowShortIfStatementsOnASingleLine: false
+AllowShortLoopsOnASingleLine: false
+AlwaysBreakAfterDefinitionReturnType: None
+AlwaysBreakAfterReturnType: None
+AlwaysBreakBeforeMultilineStrings: false
+#
+# .. but allow args/params to be packed together
+BinPackArguments: true
+BinPackParameters: true
+#
+BreakBeforeBraces: Custom
+BraceWrapping:
+  AfterCaseLabel:  false
+  AfterClass:      false
+  AfterControlStatement: Never
+  AfterEnum:       false
+  AfterFunction:   true
+  AfterNamespace:  true
+  AfterObjCDeclaration: false
+  AfterStruct:     false
+  AfterUnion:      false
+  AfterExternBlock: false
+  BeforeCatch:     false
+  BeforeElse:      false
+  BeforeLambdaBody: false
+  BeforeWhile:     false
+  IndentBraces:    false
+  SplitEmptyFunction: true
+  SplitEmptyRecord: true
+  SplitEmptyNamespace: true
+BreakBeforeBinaryOperators: None
+BreakBeforeTernaryOperators: false
+BreakConstructorInitializersBeforeComma: false
+BreakConstructorInitializers: BeforeColon
+ReflowComments:  false
+BreakStringLiterals: false
+#
+# also do some padding like Linux
+Cpp11BracedListStyle: false
+
+# Use tabs, make them width 8, like Linux
+ConstructorInitializerIndentWidth: 8
+ContinuationIndentWidth: 8
+PPIndentWidth: -1  # use IndentWidth in preprocessor
+IndentWidth: 8
+TabWidth: 8
+UseTab: Always
+
+# wide lines, never use CR
+ColumnLimit:     98
+UseCRLF: false
+
+# don't sort or merge blocks of indents
+SortIncludes: false
+IncludeBlocks:   Preserve
+
+# some more indentation config
+# don't indent case/switch or goto etc
+IndentCaseLabels: false
+IndentCaseBlocks: false
+IndentGotoLabels: false
+IndentPPDirectives: None
+IndentExternBlock: AfterExternBlock
+
+IndentWrappedFunctionNames: true
+KeepEmptyLinesAtTheStartOfBlocks: false
+
+MaxEmptyLinesToKeep: 1
+
+# whatever
+PenaltyBreakAssignment: 2
+PenaltyBreakBeforeFirstCallParameter: 19
+PenaltyBreakComment: 300
+PenaltyBreakFirstLessLess: 120
+PenaltyBreakOpenParenthesis: 0
+PenaltyBreakString: 1000
+PenaltyBreakTemplateDeclaration: 10
+PenaltyExcessCharacter: 1000000
+PenaltyReturnTypeOnItsOwnLine: 60
+PenaltyIndentedWhitespace: 0
+
+# where to place spaces
+PointerAlignment: Right
+ReferenceAlignment: Pointer
+DerivePointerAlignment: false
+SpaceAfterCStyleCast: false
+SpaceAfterLogicalNot: true
+SpaceBeforeAssignmentOperators: true
+SpaceBeforeCaseColon: false
+SpaceBeforeCpp11BracedList: false
+SpaceBeforeParens: Custom
+SpaceBeforeParensOptions:
+  AfterControlStatements: true
+  AfterForeachMacros: true
+  AfterFunctionDefinitionName: false
+  AfterFunctionDeclarationName: false
+  AfterIfMacros:   true
+  AfterOverloadedOperator: false
+  AfterRequiresInClause: false
+  AfterRequiresInExpression: false
+  BeforeNonEmptyParentheses: false
+SpaceBeforeRangeBasedForLoopColon: true
+SpaceInEmptyBlock: false
+SpaceInEmptyParentheses: false
+SpacesInAngles:  Never
+SpacesInContainerLiterals: true
+SpacesInLineCommentPrefix:
+  Minimum:         1
+  Maximum:         -1
+SpacesInParentheses: false
+SpacesInSquareBrackets: false
+SpaceBeforeSquareBrackets: false
+BitFieldColonSpacing: Both
+Standard: Cpp03
+
+DisableFormat: false

.git-blame-ignore-revs

@@ -0,0 +1,4 @@
+# (clang-format) deploy fmt
+76e01f18d0cb1d1c615077584637bce4615ccfa8
+# (clang-format) deploy fmt on casemate-check-c
+14622cb99e6dd9a2cb048d443f33be0c2a0d2099

.github/workflows/ci.yml

@@ -31,17 +31,24 @@ jobs:
       run: |
         sudo apt update
         sudo apt install build-essential
+        sudo apt install clang-format-15
 
     - name: Configure
       working-directory: rems-project/casemate
       run: |
-        ./configure
+        ./configure --clang-format=clang-format-15
+        make dump-config
 
     - name: Build all
       working-directory: rems-project/casemate
       run: |
         make
 
+    - name: clang-format
+      working-directory: rems-project/casemate
+      run: |
+        make lint
+
     - name: Run tests
       working-directory: rems-project/casemate
       run: |
@@ -109,4 +116,4 @@ jobs:
       run: |
         opam switch ${{ matrix.version }}
         eval $(opam env --switch=${{ matrix.version }})
-        make check-rocq
+        make check-rocq

Makefile

@@ -1,6 +1,8 @@
 .PHONY: build clean
 .PHONY: checks example-traces check-examples check-rocq
 .PHONY: casemate casemate-check casemate-lib
+.PHONY: fmt lint
+.PHONY: dump-config
 .PHONY: help
 
 all: casemate examples
@@ -33,6 +35,14 @@ define clean_subdir
   $(call build_subdir,CLEAN,$1,clean)
 endef
 
+define fmt_subdir
+  $(call build_subdir,FMT,$1,fmt)
+endef
+
+define lint_subdir
+  $(call build_subdir,LINT,$1,lint)
+endef
+
 # building
 
 $(subdirs): config.mk
@@ -60,3 +70,11 @@ check-examples:
 	$(call build_subdir,RUN,examples,check-examples)
 
 checks: check-examples check-rocq
+
+lint:
+	$(call lint_subdir,src/lib)
+	$(call lint_subdir,src/casemate-check-c)
+
+fmt:
+	$(call fmt_subdir,src/lib)
+	$(call fmt_subdir,src/casemate-check-c)

VERSION

@@ -0,0 +1 @@
+2.0.1-wip

configure

@@ -8,6 +8,7 @@ cc='clang'
 ld='ld'
 objdump='objdump'
 objcopy='objcopy'
+clang_format='clang-format'
 
 casemate_o="${libdir}/casemate.o"
 casemate_h="${libdir}/casemate.h"
@@ -30,6 +31,7 @@ usage() {
   echo " --ld=LD                 linker";
   echo " --arch=ARCH             machine architecture (aarch64 or x86)";
   echo " --[no-]clangd           force enable/disable clangd targets";
+  echo " --clang-format=CC       formatter";
   echo " --force                 overrule checks";
 }
 
@@ -70,6 +72,9 @@ while [[ "$1" = -* ]]; do
     --no-clangd)
         clangd=
         ;;
+    --clang-format)
+        clang_format="$arg"
+        ;;
     --force)
       force=1
       ;;
@@ -136,6 +141,8 @@ OBJDUMP = ${objdump}
 OBJCOPY = ${objcopy}
 ARCH = ${arch_name}
 
+CLANG-FORMAT = ${clang_format}
+
 CFLAGS = -Wall -MD -g -gdwarf-4 -D__${arch_name}__
 LDFLAGS =
 

src/casemate-check-c/Makefile

@@ -1,4 +1,4 @@
-.PHONY: build clean
+.PHONY: build clean fmt lint
 
 build-objs += src/opts.o
 build-objs += src/parser.o
@@ -22,3 +22,13 @@ $(root)/casemate-check: $(check-obj)
 clean:
 	$(call run_clean,$(src)/src,rm -f $(build-objs))
 	$(call run_clean,$(check-obj),rm -f $(check-obj))
+
+fmt:
+	$(call run_cmd,FMT,clang-format,\
+		$(CLANG-FORMAT) -i $$(find $(src) -iname '*.[ch]') \
+	)
+
+lint:
+	$(call run_cmd,LINT,clang-format,\
+		$(CLANG-FORMAT) --dry-run -Werror $$(find $(src) -iname '*.[ch]') \
+	)

src/casemate-check-c/include/casemate-check-impl.h

@@ -20,9 +20,9 @@ extern bool DEBUG;
 extern const char *trace_file_name;
 
 #define TRACE(FMT, ...) \
-  if (DEBUG) { \
-    fprintf(stderr, "[TRACE] %s:%u: " FMT "\n", __FILE__, __LINE__, ##__VA_ARGS__); \
-  }
+	if (DEBUG) { \
+		fprintf(stderr, "[TRACE] %s:%u: " FMT "\n", __FILE__, __LINE__, ##__VA_ARGS__); \
+	}
 
 void parse_opts(int argc, char **argv);
 

src/casemate-check-c/src/driver.c

@@ -33,7 +33,7 @@ u64 ghost_cm_read_sysreg(enum ghost_sysreg_kind sysreg)
 
 void ghost_cm_abort(const char *msg)
 {
-	if (!QUIET) {
+	if (! QUIET) {
 		if (COLOR)
 			printf(GHOST_WHITE_ON_RED);
 		printf("! %s", msg);
@@ -49,7 +49,7 @@ struct _string_buffer {
 	int n;
 };
 
-int ghost_cm_print(void* arg, const char *format, va_list ap)
+int ghost_cm_print(void *arg, const char *format, va_list ap)
 {
 	int ret;
 	if (arg != NULL) {
@@ -61,14 +61,14 @@ int ghost_cm_print(void* arg, const char *format, va_list ap)
 		buf->n -= ret;
 		return 0;
 	} else {
-		ret =vprintf(format, ap);
+		ret = vprintf(format, ap);
 		if (ret < 0)
 			return ret;
 		return 0;
 	}
 }
 
-void *ghost_cm_make_buffer(char* arg, u64 n)
+void *ghost_cm_make_buffer(char *arg, u64 n)
 {
 	struct _string_buffer *buf = malloc(sizeof(struct _string_buffer));
 	buf->buf = arg;

src/casemate-check-c/src/main.c

@@ -18,23 +18,23 @@ int main(int argc, char **argv)
 	struct casemate_model_step step;
 
 	void *parser = make_parser(f, &step);
-	while (!parser_at_EOF(parser) && !parser_at_exclamation(parser)) {
+	while (! parser_at_EOF(parser) && ! parser_at_exclamation(parser)) {
 		parse_record(parser);
 		casemate_model_step(step);
 	}
 
 	if (parser_at_exclamation(parser)) {
 		/* logfile claimed there was an error here ... */
-		fprintf(stderr, "! casemate-check: mismatch between success status, logfile had violation but none detected.\n");
+		fprintf(stderr,
+			"! casemate-check: mismatch between success status, logfile had violation but none detected.\n");
 		ret = 1;
 	} else {
 		/* at EOF:
 		 * no more transitions, steps had no errors, all good! !*/
-		 fprintf(stderr, "casemate-check: log checked successfully.\n");
-		 ret = 0;
+		fprintf(stderr, "casemate-check: log checked successfully.\n");
+		ret = 0;
 	}
 
-
 	free(parser);
 	free(st);