From 7830be310ab1e0cda7dab2ee16a10b82c1ee0180 Mon Sep 17 00:00:00 2001 From: Tom Wallis Date: Mon, 29 Sep 2025 14:39:29 +0100 Subject: [PATCH 1/7] Remove original CIL --- .gitmodules | 3 --- contrib/cil | 1 - 2 files changed, 4 deletions(-) delete mode 160000 contrib/cil diff --git a/.gitmodules b/.gitmodules index ccc214c8..240bffc8 100644 --- a/.gitmodules +++ b/.gitmodules @@ -16,9 +16,6 @@ [submodule "contrib/donald"] path = contrib/donald url = https://github.com/stephenrkell/donald.git -[submodule "contrib/cil"] - path = contrib/cil - url = https://github.com/stephenrkell/cil.git [submodule "contrib/elftin"] path = contrib/elftin url = https://github.com/stephenrkell/elftin.git diff --git a/contrib/cil b/contrib/cil deleted file mode 160000 index 96c0ecae..00000000 --- a/contrib/cil +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 96c0ecae32443c4705bad6eaf2410c65f6916bd2 From 43eec0dfd5bc2c9b34d103e756314e06002cf23f Mon Sep 17 00:00:00 2001 From: Tom Wallis Date: Thu, 23 Oct 2025 18:48:44 +0100 Subject: [PATCH 2/7] goblint/cil liballocs with fixed makefiles, working `allocscc` --- contrib/cil | 1 + contrib/elftin | 2 +- contrib/toolsub | 2 +- tools/lang/c/Makefile | 19 +++-- tools/lang/c/bin/allocscc | 11 +-- tools/lang/c/cilallocs/cilallocs.ml | 37 +++++----- tools/lang/c/dumpallocs/dumpallocs.ml | 79 ++++++++++----------- tools/lang/c/dumpmemacc/dumpmemacc.ml | 6 +- tools/lang/c/monalloca/monalloca.ml | 12 ++-- tools/lang/c/trapptrwrites/trapptrwrites.ml | 22 +++--- 10 files changed, 98 insertions(+), 93 deletions(-) create mode 160000 contrib/cil diff --git a/contrib/cil b/contrib/cil new file mode 160000 index 00000000..46078e18 --- /dev/null +++ b/contrib/cil @@ -0,0 +1 @@ +Subproject commit 46078e18e855498043d757781b2d3fbf1ea7c514 diff --git a/contrib/elftin b/contrib/elftin index b3fc5e21..1369e841 160000 --- a/contrib/elftin +++ b/contrib/elftin @@ -1 +1 @@ -Subproject commit b3fc5e219a371083bd10c72dc8fcee3373f178a2 +Subproject commit 1369e841128f2b7f519b3fd1683e8efc2b8f8fa6 diff --git a/contrib/toolsub b/contrib/toolsub index 601bb206..fa1b495d 160000 --- a/contrib/toolsub +++ b/contrib/toolsub @@ -1 +1 @@ -Subproject commit 601bb2062337a981796c576e4884c8ca1c333192 +Subproject commit fa1b495ddd432cc9b378774ca78f1b99d46fd3e2 diff --git a/tools/lang/c/Makefile b/tools/lang/c/Makefile index b88f4709..7af00743 100644 --- a/tools/lang/c/Makefile +++ b/tools/lang/c/Makefile @@ -6,10 +6,14 @@ OCAMLFIND ?= ocamlfind ifeq ($(CIL_INSTALL),) $(error "Expected CIL_INSTALL to be set") endif +ifeq ($(CIL_ROOT),) +$(error "Expected CIL_ROOT to be set") +endif CILLY ?= $(CIL_INSTALL)/../bin/cilly CIL_TOOLS ?= cilallocs dumpallocs monalloca dumpmemacc trapptrwrites -OCAMLFLAGS += -package findlib -OCAMLFLAGS += -I $(CIL_INSTALL)/cil -I $(dir $(THIS_MAKEFILE))/cilallocs +OCAMLFLAGS += -package findlib -package goblint-cil +OCAMLFLAGS += -I $(dir $(THIS_MAKEFILE))/cilallocs +OCAMLFLAGS += -open GoblintCil -open GoblintCil.Cilint CIL_TOOLS_SRC := $(shell find $(CIL_TOOLS) $(realpath $(dir $(THIS_MAKEFILE)))/lib -name '*.ml') @@ -24,13 +28,14 @@ DEPS += $(OCAML_DEPS) -include $(DEPS) %.cmxs: %.cmx - $(OCAMLFIND) ocamlopt -shared -o "$@" $(OCAMLOPTFLAGS) $(OCAMLFLAGS) $+ + eval \$\(opam env --switch=${CIL_ROOT} --set-switch\) && $(OCAMLFIND) ocamlopt -shared -o "$@" $(OCAMLOPTFLAGS) $(OCAMLFLAGS) $+ %.cmx %.cmi: %.ml - $(OCAMLFIND) ocamlopt -o "$@" $(OCAMLOPTFLAGS) $(OCAMLFLAGS) -c "$<" + eval \$\(opam env --switch=${CIL_ROOT} --set-switch\) && $(OCAMLFIND) ocamlopt -o "$@" $(OCAMLOPTFLAGS) $(OCAMLFLAGS) -c "$<" +goblintCil.cmo: goblintCil.ml ; %.cmo %.cmi: %.ml - $(OCAMLFIND) ocamlc -o "$@" $(OCAMLFLAGS) -c "$<" + eval \$\(opam env --switch=${CIL_ROOT} --set-switch\) && $(OCAMLFIND) ocamlc -o "$@" $(OCAMLFLAGS) -c "$<" %.cma: %.cmo - $(OCAMLFIND) ocamlc -o "$@" $(OCAMLFLAGS) -a $+ + eval \$\(opam env --switch=${CIL_ROOT} --set-switch\) && $(OCAMLFIND) ocamlc -o "$@" $(OCAMLFLAGS) -a $+ # build cilallocs first dumpallocs/dumpallocs.cmx: cilallocs/cilallocs.cmx @@ -46,4 +51,4 @@ monalloca/monalloca.cmo: cilallocs/cilallocs.cmo .PHONY: clean clean: - for dir in $(CIL_TOOLS); do (cd $$dir && rm -f *.o *.cmo *.cma *.cmi *.cmx *.cmxa *.cmxs *.cil.c *.i ); done + for dir in $(CIL_TOOLS); do (cd $$dir && rm -f *.o *.cmo *.cma *.cmi *.cmx *.cmxa *.cmxs *.cil.c *.i *.d ); done diff --git a/tools/lang/c/bin/allocscc b/tools/lang/c/bin/allocscc index 3dc910b9..2ded7e16 100755 --- a/tools/lang/c/bin/allocscc +++ b/tools/lang/c/bin/allocscc @@ -12,14 +12,15 @@ import os, sys, re, subprocess, tempfile REAL_FILE = os.path.realpath(__file__) REAL_DIR = os.path.realpath(os.path.dirname(REAL_FILE)) liballocs_base = os.path.realpath(REAL_DIR + "/../../../..") +cil_base = os.environ.get("CIL_ROOT", liballocs_base + "/contrib/cil/") sys.path.append(liballocs_base + "/tools") from allocscompilerwrapper import * existing_cil_install = os.environ.get("CIL_INSTALL") -if existing_cil_install == None: - cilly_cmd = liballocs_base + "/contrib/cil/bin/cilly" - existing_cil_install = liballocs_base + "/contrib/cil/lib" +if cil_base == None: + cilly_cmd = liballocs_base + "/_build/install/default/bin/cilly" + existing_cil_install = liballocs_base + "/contrib/cil/_build/install/default/lib/goblint-cil/" else: - cilly_cmd = existing_cil_install + "/../bin/cilly" + cilly_cmd = cil_base + "/_build/install/default/bin/cilly" existing_elftin = os.environ.get("ELFTIN") if existing_elftin == None: os.putenv("ELFTIN", liballocs_base + "/contrib/elftin") @@ -96,7 +97,7 @@ class AllocsCC(AllocsCompilerWrapper): return [ "--save-temps", "--decil", - "--native", + #"--native", "--load=%s" % (self.getLibAllocsBaseDir() + "/tools/lang/c/cilallocs/cilallocs.cmxs"), "--load=%s" % (self.getLibAllocsBaseDir() + "/tools/lang/c/dumpallocs/dumpallocs.cmxs"), "--dodumpallocs", diff --git a/tools/lang/c/cilallocs/cilallocs.ml b/tools/lang/c/cilallocs/cilallocs.ml index a3c4eb8c..29c4a20d 100644 --- a/tools/lang/c/cilallocs/cilallocs.ml +++ b/tools/lang/c/cilallocs/cilallocs.ml @@ -43,7 +43,6 @@ open Unix open List open Str open Map -open Pretty open Cil open Hashtbl module NamedTypeMap = Map.Make(String) @@ -169,7 +168,7 @@ let unzip l = let foldConstants e = visitCilExpr (Cil.constFoldVisitor true) e -let makeIntegerConstant n = Const(CInt64(n, IInt, None)) +let makeIntegerConstant n = Const(CInt(n, IInt, None)) let isStaticallyZero e = isZero (foldConstants e) @@ -186,8 +185,8 @@ let rec isStaticallyNull e = isStaticallyZero e || isStaticallyNullPtr e let constInt64ValueOfExprNoChr (intExp: Cil.exp) : int64 option = match (foldConstants intExp) with - Const(CInt64(intValue, _, _)) -> - Some(intValue) + Const(CInt(intValue, _, _)) -> + Some(int64_of_cilint intValue) | _ -> None let constInt64ValueOfExpr (intExp: Cil.exp) : int64 option = @@ -196,9 +195,9 @@ let constInt64ValueOfExpr (intExp: Cil.exp) : int64 option = | _ -> constInt64ValueOfExprNoChr intExp let nullPtr = CastE( TPtr(TVoid([]), []) , zero ) -let one = Const(CInt64((Int64.of_int 1), IInt, None)) +let one = Const(CInt((cilint_of_int64 (Int64.of_int 1)), IInt, None)) let onePtr = CastE( TPtr(TVoid([]), []) , one ) -let negativeOne = Const(CInt64((Int64.of_int (0-1)), IInt, None)) +let negativeOne = Const(CInt(cilint_of_int64 (Int64.of_int (0-1)), IInt, None)) let negativeOnePtr = CastE( TPtr(TVoid([]), []) , negativeOne ) let debug_print lvl s = @@ -208,7 +207,7 @@ let debug_print lvl s = int_of_string levelString end with Not_found -> 0 | Failure(_) -> 0 in - if level >= lvl then (output_string Pervasives.stderr s; flush Pervasives.stderr) else () + if level >= lvl then (output_string Out_channel.stderr s; flush Out_channel.stderr) else () (* HACKed realpath for now: *) let abspath f = @@ -229,8 +228,8 @@ let trim str = in let len = String.length str in try - let left = search_pos 0 (fun i -> i >= len) (succ) - and right = search_pos (len - 1) (fun i -> i < 0) (pred) + let left = search_pos 0 (fun i -> i >= len) (Stdlib.succ) + and right = search_pos (len - 1) (fun i -> i < 0) (Stdlib.pred) in String.sub str left (right - left + 1) with Empty -> "" @@ -287,7 +286,7 @@ let rec barenameFromSig ts = "__ARG" ^ (string_of_int startAt) ^ "_" ^ (barenameFromSig t) ^ remainder in match ts with - TSArray(tNestedSig, optSz, attrs) -> "__ARR" ^ (match optSz with Some(s) -> (string_of_int (i64_to_int s)) | None -> "0") ^ "_" ^ (barenameFromSig tNestedSig) + TSArray(tNestedSig, optSz, attrs) -> "__ARR" ^ (match optSz with Some(s) -> (string_of_int (i64_to_int (int64_of_cilint s))) | None -> "0") ^ "_" ^ (barenameFromSig tNestedSig) | TSPtr(tNestedSig, attrs) -> "__PTR_" ^ (barenameFromSig tNestedSig) | TSComp(isSpecial, name, attrs) -> name | TSFun(returnTs, Some(argsTss), false, attrs) -> @@ -315,7 +314,7 @@ let rec dwarfidlFromSig ts = match ts with TSArray(tNestedSig, optSz, attrs) -> "(array_type [type = " ^ (dwarfidlFromSig tNestedSig) ^ "] {" - ^ (match optSz with Some(s) -> ("subrange_type [upper_bound = " ^ (string_of_int (i64_to_int s)) ^ "];") | None -> "") ^ " })" + ^ (match optSz with Some(s) -> ("subrange_type [upper_bound = " ^ (string_of_int (i64_to_int (int64_of_cilint s))) ^ "];") | None -> "") ^ " })" | TSPtr(tNestedSig, attrs) -> "(pointer_type [type = " ^ (dwarfidlFromSig tNestedSig) ^ "];)" | TSComp(isSpecial, name, attrs) -> name | TSFun(returnTs, Some(argsTss), false, attrs) -> @@ -366,7 +365,7 @@ let rec decayArrayInTypesig ts = match ts with let rec accumulateArrayDimensionsInTypesig ts = match ts with TSArray(tsig, Some(sz), attrs) -> (* recurse for multidim arrays *) (match accumulateArrayDimensionsInTypesig tsig with - (ts, Some(subN)) -> (ts, Some(Int64.mul sz subN)) + (ts, Some(subN)) -> (ts, Some(Int64.mul (int64_of_cilint sz) subN)) | (ts, None) -> (ts, None) ) | TSArray(tsig, None, attrs) -> (* recurse for multidim arrays *) @@ -380,7 +379,7 @@ let rec collapseArrayDimensionsInTypesig ts = match ts with -> (* tsig is also an array, so ... *) let ts, maybeSz = accumulateArrayDimensionsInTypesig ts in - TSArray(ts, maybeSz, attrs) + TSArray(ts, Option.map cilint_of_int64 maybeSz, attrs) | _ -> ts (* This will make a "pointer to array of X" typesig into a "pointer to X" typesig. @@ -557,7 +556,7 @@ let getOrCreateUniqtypeGlobal m concreteType globals = tempGlobal.vattr <- [Attr("weak", [])]; tempGlobal in - let newGlobalVarInfo = GVarDecl(newGlobal, {line = -1; file = "BLAH FIXME"; byte = 0}) + let newGlobalVarInfo = GVarDecl(newGlobal, {line = -1; file = "BLAH FIXME"; byte = 0; column = -1; endLine = -1; endByte = -1; endColumn = -1; synthetic = false }) in let newMap = (UniqtypeMap.add concreteType newGlobalVarInfo m) in @@ -652,7 +651,7 @@ let findOrCreateExternalFunctionInFile fl nm proto : fundec = (* findOrCreateFun Some(d) -> d | None -> let funDec = emptyFunction nm in funDec.svar.vtype <- proto; - fl.globals <- newGlobalsList fl.globals [GVarDecl(funDec.svar, {line = -1; file = "BLAH FIXME"; byte = 0})] isFunction; + let loc = {line = -1; file = "BLAH FIXME"; byte = 0; column = -1; endLine = -1; endByte = -1; endColumn = -1; synthetic = false } in funDec let findOrCreateNewFunctionInFile fl nm proto l createBeforePred : fundec = (* findOrCreateFunc fl nm proto *) (* NO! doesn't let us have the fundec *) @@ -677,7 +676,7 @@ let makeInlineFunctionInFile fl ourFun nm proto body referencedValues = begin let arglist = List.map (fun (ident, typ, attrs) -> makeFormalVar ourFun ident typ) protoArgs in let () = setFunctionType ourFun protoWithInlineAttrs in let nameFunc = (fun n t -> makeTempVar ourFun ~name:n t) in - let loc = {line = -1; file = "BLAH FIXME"; byte = 0} in + let loc = {line = -1; file = "BLAH FIXME"; byte = 0; column = -1; endLine = -1; endByte = -1; endColumn = -1; synthetic = false } in let argPatternBindings = List.map (fun ((ident, typ, attrs), arg) -> (ident, Fv arg)) (List.combine protoArgs arglist) in let extPatternBindings = (* List.map (fun (ident, v) -> (ident, Fv v)) *) referencedValues in let madeBody = mkBlock (Formatcil.cStmts body nameFunc loc (argPatternBindings @ extPatternBindings)) in @@ -826,7 +825,8 @@ let restructureInstrsStatement skind = Instr(group); sid = 0; succs = []; - preds = [] + preds = []; + fallthrough = None }] }) in @@ -835,7 +835,8 @@ let restructureInstrsStatement skind = skind; sid = 0; succs = []; - preds = [] + preds = []; + fallthrough = None } ) groupedInstrs) in let b = mkBlock stmts in diff --git a/tools/lang/c/dumpallocs/dumpallocs.ml b/tools/lang/c/dumpallocs/dumpallocs.ml index 1227a67c..cab37c27 100644 --- a/tools/lang/c/dumpallocs/dumpallocs.ml +++ b/tools/lang/c/dumpallocs/dumpallocs.ml @@ -87,7 +87,7 @@ let maybeDecayArrayTypesig maybeTs = match maybeTs with | _ -> Undet let rec getSizeExpr (ex: exp) (env : (int * sz) list) (gs : Cil.global list) : sz = - debug_print 1 ("Hello from getSizeExpr(" ^ (Pretty.sprint 80 (Pretty.dprintf "%a" d_exp ex)) ^ ") ... "); flush Pervasives.stderr; + debug_print 1 ("Hello from getSizeExpr(" ^ (Pretty.sprint 80 (Pretty.dprintf "%a" d_exp ex)) ^ ") ... "); flush Out_channel.stderr; let isTrailingField fi compinfo = let reverseFields = rev compinfo.cfields in @@ -112,17 +112,17 @@ let rec getSizeExpr (ex: exp) (env : (int * sz) list) (gs : Cil.global list) : s * &a.i[0] a.k.a. &a.i a.k.a. a.i * might be a trailing field, if i is the last field in the struct. *) let rec isTrailingFieldOffsetExpr ts off = - debug_print 1 ("Hello from isTrailingFieldOffsetExpr(" ^ (Pretty.sprint 80 (d_typsig () ts)) ^ (Pretty.sprint 80 (d_offset Pretty.nil () off)) ^ ") "); flush Pervasives.stderr; + debug_print 1 ("Hello from isTrailingFieldOffsetExpr(" ^ (Pretty.sprint 80 (d_typsig () ts)) ^ (Pretty.sprint 80 (d_offset Pretty.nil () off)) ^ ") "); flush Out_channel.stderr; match off with - NoOffset -> (debug_print 1 ("... no offset\n"); flush Pervasives.stderr; false) + NoOffset -> (debug_print 1 ("... no offset\n"); flush Out_channel.stderr; false) | Field(fi, NoOffset) when isTrailingField fi fi.fcomp - -> (debug_print 1 ("... trailing field + no offset\n"); flush Pervasives.stderr; true) + -> (debug_print 1 ("... trailing field + no offset\n"); flush Out_channel.stderr; true) | Field(fi, NoOffset) - -> (debug_print 1 ("... non-trailing no-offset\n"); flush Pervasives.stderr; false) + -> (debug_print 1 ("... non-trailing no-offset\n"); flush Out_channel.stderr; false) | Index(indexEx, maybeOffset) - -> (debug_print 1 ("... index\n"); flush Pervasives.stderr; isTrailingFieldOffsetExpr (arrayElementType ts) maybeOffset) + -> (debug_print 1 ("... index\n"); flush Out_channel.stderr; isTrailingFieldOffsetExpr (arrayElementType ts) maybeOffset) | Field(fi, someOffset) - -> (debug_print 1 ("... residual field case\n"); flush Pervasives.stderr; isTrailingFieldOffsetExpr (typeSig fi.ftype) someOffset) + -> (debug_print 1 ("... residual field case\n"); flush Out_channel.stderr; isTrailingFieldOffsetExpr (typeSig fi.ftype) someOffset) (* (getConcreteType (typeSig fi.ftype)) = (getConcreteType ts) -> @@ -138,7 +138,7 @@ let rec getSizeExpr (ex: exp) (env : (int * sz) list) (gs : Cil.global list) : s *) in let containingTypeSigInTrailingFieldOffsetFromNullPtrExpr lv = begin - debug_print 1 ("Hello from containingTypeSigInTrailingFieldOffsetFromNullPtrExpr(" ^ (Pretty.sprint 80 (Pretty.dprintf "%a" d_lval lv)) ^ ")\n"); flush Pervasives.stderr; + debug_print 1 ("Hello from containingTypeSigInTrailingFieldOffsetFromNullPtrExpr(" ^ (Pretty.sprint 80 (Pretty.dprintf "%a" d_lval lv)) ^ ")\n"); flush Out_channel.stderr; match lv with (* Does it make sense to have complex expressions when doing an offsetof-based size calculation? e.g. @@ -161,18 +161,18 @@ let rec getSizeExpr (ex: exp) (env : (int * sz) list) (gs : Cil.global list) : s Field(d-fieldinfo, NoOffset))))))) *) - (Mem(e), off) -> debug_print 1 ("Saw Mem case\n"); flush Pervasives.stderr; + (Mem(e), off) -> debug_print 1 ("Saw Mem case\n"); flush Out_channel.stderr; if isStaticallyNullPtr e then ( debug_print 1 ("Saw statically-null case\n"); - flush Pervasives.stderr; + flush Out_channel.stderr; let targetTs = pointerTargetType (typeSig (typeOf e)) in if isTrailingFieldOffsetExpr targetTs off then Some(targetTs) else None ) - else (debug_print 1 ("Saw non-statically-null case\n"); flush Pervasives.stderr; None) + else (debug_print 1 ("Saw non-statically-null case\n"); flush Out_channel.stderr; None) | _ -> None end in @@ -268,14 +268,14 @@ let rec getSizeExpr (ex: exp) (env : (int * sz) list) (gs : Cil.global list) : s if ci.cstruct && List.length ci.cfields > 0 then let fi = List.nth ci.cfields (List.length ci.cfields - 1) in - let _ = (debug_print 1 ("Hello from field-subtracting (s - f) case in getSizeExpr (s is " ^ (typsigToString ts1) ^ ", f is " ^ (typToString fi.ftype) ^ " )\n"); flush Pervasives.stderr) in + let _ = (debug_print 1 ("Hello from field-subtracting (s - f) case in getSizeExpr (s is " ^ (typsigToString ts1) ^ ", f is " ^ (typToString fi.ftype) ^ " )\n"); flush Out_channel.stderr) in let subtractingLastField = if fi.fbitfield <> None then false else (let tsf = Cil.typeSig fi.ftype in tsMatchModuloSignedness tsf ts2 || (match tsf with - TSArray(tsa, Some(bound), _) when bound = Int64.one -> + TSArray(tsa, Some(bound), _) when bound = cilint_of_int64 Int64.one -> tsMatchModuloSignedness tsa ts2 | ts -> false) ) @@ -308,7 +308,7 @@ let rec getSizeExpr (ex: exp) (env : (int * sz) list) (gs : Cil.global list) : s end | CastE(t, e) -> (getSizeExpr e env gs) (* i.e. recurse down e *) | AddrOf(lv) -> begin - debug_print 1 ("Hello from AddrOf case in getSizeExpr\n"); flush Pervasives.stderr; + debug_print 1 ("Hello from AddrOf case in getSizeExpr\n"); flush Out_channel.stderr; let ts = containingTypeSigInTrailingFieldOffsetFromNullPtrExpr lv in match ts with None -> Undet @@ -329,7 +329,7 @@ let rec getSizeExpr (ex: exp) (env : (int * sz) list) (gs : Cil.global list) : s | Undet -> debug_print 1 "don't know\n" | TooComplex -> debug_print 1 "something too complex\n" ); - flush Pervasives.stderr; + flush Out_channel.stderr; res ) @@ -380,35 +380,35 @@ let matchUserAllocArgs i arglist signature env maybeFunNameToPrint (calledFuncti in let fragment = (* string_after *) (matched_string signature) (* nskip *) in - (debug_print 1 ("Info: signature " ^ signature ^ " did contain a function arg spec (" ^ fragment ^ " a.k.a. signature + "^ (string_of_int nskip) ^")\n"); flush Pervasives.stderr); + (debug_print 1 ("Info: signature " ^ signature ^ " did contain a function arg spec (" ^ fragment ^ " a.k.a. signature + "^ (string_of_int nskip) ^")\n"); flush Out_channel.stderr); fragment ) with Not_found -> ( - (debug_print 1 ("Warning: signature " ^ signature ^ " did not contain an arg spec\n"); flush Pervasives.stderr); + (debug_print 1 ("Warning: signature " ^ signature ^ " did not contain an arg spec\n"); flush Out_channel.stderr); "" ) in let sizeArgPos = if string_match (regexp "[^A-Z]*[A-Z]") signatureArgSpec 0 then Some((String.length (matched_string signatureArgSpec)) - 1 (* for the bracket*) - 1 (* because we want zero-based *)) - else (debug_print 1 ("Warning: signature " ^ signature ^ " did not contain a capitalized arg spec element\n"); flush Pervasives.stderr; None) + else (debug_print 1 ("Warning: signature " ^ signature ^ " did not contain a capitalized arg spec element\n"); flush Out_channel.stderr; None) in match sizeArgPos with Some(s) -> if (length arglist) > s then let szEx = - (debug_print 1 ("Looking at arg expression number " ^ (string_of_int s) ^ "\n"); flush Pervasives.stderr); + (debug_print 1 ("Looking at arg expression number " ^ (string_of_int s) ^ "\n"); flush Out_channel.stderr); getSizeExpr (nth arglist s) env gs in match szEx with - Existing(szType, _) -> (debug_print 1 ("Inferred that we are allocating some number of " ^ (Pretty.sprint 80 (Pretty.dprintf "\t%a\t" d_typsig szType)) ^ "\n"); flush Pervasives.stderr ); + Existing(szType, _) -> (debug_print 1 ("Inferred that we are allocating some number of " ^ (Pretty.sprint 80 (Pretty.dprintf "\t%a\t" d_typsig szType)) ^ "\n"); flush Out_channel.stderr ); szEx - | Undet | TooComplex -> debug_print 1 ("Could not infer what we are allocating\n"); flush Pervasives.stderr; szEx - | Synthetic(_) -> debug_print 1 ("We are allocating a composite: FIXME print this out\n"); flush Pervasives.stderr; szEx + | Undet | TooComplex -> debug_print 1 ("Could not infer what we are allocating\n"); flush Out_channel.stderr; szEx + | Synthetic(_) -> debug_print 1 ("We are allocating a composite: FIXME print this out\n"); flush Out_channel.stderr; szEx else (match maybeFunNameToPrint with Some(fnname) -> ((debug_print 1 ("Warning: signature " ^ signature ^ " wrongly predicts allocation function " ^ fnname ^ " will have at least " ^ (string_of_int s) ^ " arguments, where call site it has only " ^ (string_of_int (length arglist)) ^"\n"); - flush Pervasives.stderr); Undet) + flush Out_channel.stderr); Undet) | None -> (debug_print 1 ("Warning: spec argument count (" ^ (string_of_int s) ^ ") does not match call-site argument count (" ^ (string_of_int (length arglist)) ^ ")")); Undet) | None -> (* If we have no sizearg pos, use the return type of the function: @@ -456,10 +456,10 @@ let functionNameMatchesSignature fname signature = match friendlyName with Some(s) -> (debug_print 1 ("Info: signature " ^ signature ^ " did contain a function name: " ^ s ^ "\n"); - flush Pervasives.stderr; + flush Out_channel.stderr; fname = s ) | None -> (debug_print 1 ("Warning: signature " ^ signature ^ " did not contain a function name\n"); - flush Pervasives.stderr; false ) + flush Out_channel.stderr; false ) let functionArgCountMatchesSignature arglist signature = let (friendlyName, friendlyArgChars) = parseSignature signature @@ -471,7 +471,7 @@ let rec extractUserAllocMatchingSignature i maybeFunName arglist signature env ( (* destruct the signature string *) debug_print 1 ("Warning: matching against signature " ^ signature ^ " when argcount is " ^ (string_of_int (List.length arglist)) ^ "\n"); - flush Pervasives.stderr; + flush Out_channel.stderr; match maybeFunName with Some(fname) when functionNameMatchesSignature fname signature @@ -607,8 +607,8 @@ let rec accumulateOverStatements acc (stmts: Cil.stmt list) (gs : Cil.global lis Let's try this. *) let rec accumulateOverOneInstr acc i = (* debug_print 1 "hello from accumulateOverOneInstr\n"; flush Pervasives.stderr; *) match i with - Call(_, f, args, l) -> acc - | Set((host, off), e, l) -> begin + Call(_, f, args, l, _) -> acc + | Set((host, off), e, l, _) -> begin match host with Var(v) -> if v.vglob then acc else begin let szness = getSizeExpr e acc gs in @@ -616,7 +616,7 @@ let rec accumulateOverStatements acc (stmts: Cil.stmt list) (gs : Cil.global lis Undet -> acc | _ -> ( debug_print 1 ("found some sizeofness in assignment to: " ^ (Pretty.sprint 80 (Pretty.dprintf "\t%a\t" d_lval (host, off))) ^ " (vid " ^ (string_of_int v.vid) ^ ", sizeofness " ^ (sizeofnessToString szness) ^ ")\n"); - flush Pervasives.stderr; + flush Out_channel.stderr; (v.vid, szness) :: (remove_assoc v.vid acc)) end | Mem(e) -> acc @@ -642,12 +642,9 @@ let rec accumulateOverStatements acc (stmts: Cil.stmt list) (gs : Cil.global lis | Continue (l : location) -> *) | Block(b) -> (* recurse over the block's stmts *) accumulateOverStatements acc b.bstmts gs - | If (e, b1, b2, l) -> accumulateOverStatements (accumulateOverStatements acc b2.bstmts gs) b1.bstmts gs - | Switch (e, b, ss, l) -> accumulateOverStatements (accumulateOverStatements acc ss gs) b.bstmts gs - | Loop (b, l, continueLabel, breakLabel) -> accumulateOverStatements acc b.bstmts gs - | TryFinally (tryBlock, finallyBlock, l) -> accumulateOverStatements (accumulateOverStatements acc tryBlock.bstmts gs) finallyBlock.bstmts gs - | TryExcept (tryBlock, _, exceptBlock, l) - -> accumulateOverStatements (accumulateOverStatements acc tryBlock.bstmts gs) exceptBlock.bstmts gs (* FIXME: instr list doesn't get handled*) + | If (e, b1, b2, l, _) -> accumulateOverStatements (accumulateOverStatements acc b2.bstmts gs) b1.bstmts gs + | Switch (e, b, ss, l, _) -> accumulateOverStatements (accumulateOverStatements acc ss gs) b.bstmts gs + | Loop (b, l, _, continueLabel, breakLabel) -> accumulateOverStatements acc b.bstmts gs | _ -> acc in match stmts with @@ -685,7 +682,7 @@ class dumpAllocsVisitor = fun (fl: Cil.file) -> object(self) (* debug_print 1 ("printing alloc for " ^ fileAndLine ^ ", funvar " ^ funvar.vname ^ "\n"); *) let chan = match !outChannel with | Some(s) -> s - | None -> Pervasives.stderr + | None -> Out_channel.stderr in let targetFunc = match maybeFunvar with Some(funvar) -> Pretty.sprint 80 (* I so do not understand Pretty.dprintf *) @@ -767,12 +764,12 @@ class dumpAllocsVisitor = fun (fl: Cil.file) -> object(self) method vinst (i: instr) : instr list visitAction = ( debug_print 1 ("considering instruction " ^ ( match i with - Call(_, _, _, l) -> "(call) at " ^ l.file ^ ", line: " ^ (string_of_int l.line) - | Set(_, _, l) -> "(assignment) at " ^ l.file ^ ", line: " ^ (string_of_int l.line) + Call(_, _, _, l, _) -> "(call) at " ^ l.file ^ ", line: " ^ (string_of_int l.line) + | Set(_, _, l, _) -> "(assignment) at " ^ l.file ^ ", line: " ^ (string_of_int l.line) | Asm(_, _, _, _, _, l) -> "(assembly) at " ^ l.file ^ ", line: " ^ (string_of_int l.line) - ) ^ "\n"); flush Pervasives.stderr); + ) ^ "\n"); flush Out_channel.stderr); match i with - Call(_, funExpr, args, l) -> begin + Call(_, funExpr, args, l, _) -> begin let handleCall maybeFunvar (functionT : Cil.typ) = begin let functionTs = typeSig functionT in match functionTs with @@ -849,7 +846,7 @@ class dumpAllocsVisitor = fun (fl: Cil.file) -> object(self) | _ (* match f *) -> (debug_print 1 ("skipping call to non-lvalue at " ^ l.file ^ ":" ^ (string_of_int l.line) ^ "\n"); flush Pervasives.stderr; SkipChildren) *) end - | Set(lv, e, l) -> (* (debug_print 1 ("skipping assignment at " ^ l.file ^ ":" ^ (string_of_int l.line) ^ "\n" ); flush Pervasives.stderr; *) SkipChildren (* ) *) + | Set(lv, e, l, _) -> (* (debug_print 1 ("skipping assignment at " ^ l.file ^ ":" ^ (string_of_int l.line) ^ "\n" ); flush Pervasives.stderr; *) SkipChildren (* ) *) | Asm(_, _, _, _, _, l) -> (* (debug_print 1 ("skipping assignment at " ^ l.file ^ ":" ^ (string_of_int l.line) ^ "\n" ); *) SkipChildren (* ) *) (* ) *) end (* class dumpAllocsVisitor *) diff --git a/tools/lang/c/dumpmemacc/dumpmemacc.ml b/tools/lang/c/dumpmemacc/dumpmemacc.ml index 5bceb49c..e370f15f 100644 --- a/tools/lang/c/dumpmemacc/dumpmemacc.ml +++ b/tools/lang/c/dumpmemacc/dumpmemacc.ml @@ -16,7 +16,7 @@ class dumpMemAccVisitor = fun (fl: Cil.file) -> object(self) method doReport (direction : string) (kind: string) (exprT : Cil.typ) (enclosingT : Cil.typ) : unit = let chan = match !outChannel with Some(c) -> c - | None -> Pervasives.stderr + | None -> Out_channel.stderr in let loc = match !currentLoc with Some(l) -> l @@ -117,7 +117,7 @@ class dumpMemAccVisitor = fun (fl: Cil.file) -> object(self) method vinst (outerI: instr) : instr list visitAction = ChangeDoChildrenPost([outerI], fun is -> match is with - [Call(maybeOut, funExpr, args, l)] -> ( + [Call(maybeOut, funExpr, args, l, _)] -> ( currentLoc := Some(l); (match maybeOut with Some(lv) -> self#reportWrite lv @@ -126,7 +126,7 @@ class dumpMemAccVisitor = fun (fl: Cil.file) -> object(self) let _ = List.mapi (fun idx -> (fun subE -> (self#reportVirtualWrite subE))) args in (); is ) - | [Set(lv, e, l)] -> + | [Set(lv, e, l, _)] -> currentLoc := Some(l); self#reportVirtualWrite e; self#reportWrite lv; diff --git a/tools/lang/c/monalloca/monalloca.ml b/tools/lang/c/monalloca/monalloca.ml index 65e7168f..37fb2faf 100644 --- a/tools/lang/c/monalloca/monalloca.ml +++ b/tools/lang/c/monalloca/monalloca.ml @@ -91,7 +91,7 @@ let ensureCleanupLocal (fn : fundec) = (* trying to initialize this right here, by adding to fn.sbody.bstmts, doesn't work -- likely because it gets clobbered by the visitor code. So we do it when visiting the function instead. *) - fn.sbody.bstmts <- (mkStmtOneInstr (Set((Var(v), NoOffset), zero, v.vdecl))) + fn.sbody.bstmts <- (mkStmtOneInstr (Set((Var(v), NoOffset), zero, v.vdecl, v.vdecl))) :: fn.sbody.bstmts; v @@ -114,7 +114,7 @@ class monAllocaExprVisitor = fun (fl: Cil.file) | _ -> false in match i with - Call(tgt, funExpr, [sizeArg], l) when isAllocaFun funExpr -> begin + Call(tgt, funExpr, [sizeArg], l, _) when isAllocaFun funExpr -> begin (* We need to * - ensure we have a local in the function for recording the fact that this frame does alloca @@ -156,7 +156,7 @@ class monAllocaExprVisitor = fun (fl: Cil.file) ChangeTo([ Call(Some(Var(fixedSizeVar), NoOffset), Lval(Var(liballocsAllocaSizeFun.svar), NoOffset), - [sizeArg], l); + [sizeArg], l, l); Asm([(* attrs *)], [(* template strings *) " call "^ labelString1 ^"_%=\n\ @@ -170,14 +170,14 @@ class monAllocaExprVisitor = fun (fl: Cil.file) [(* clobbers *)], (* location *) l ); Call(Some(Var(tempPtrVar), NoOffset), Lval(Var(builtinAllocaFunVar), NoOffset), - [Lval(Var(fixedSizeVar), NoOffset)], l); + [Lval(Var(fixedSizeVar), NoOffset)], l, l); Call(tgt, Lval(Var(liballocsNotifyAndAdjustAllocaFun.svar), NoOffset), [Lval(Var(tempPtrVar), NoOffset); sizeArg; Lval(Var(fixedSizeVar), NoOffset); mkAddrOf (Var(counterVar), NoOffset); Lval(Var(callSiteVar), NoOffset) - ], l) + ], l, l) ]) end | _ -> SkipChildren @@ -236,7 +236,7 @@ class monAllocaFunVisitor = fun (fl: Cil.file) -> object(self) None -> ChangeTo(modifiedFunDec) | Some(v) -> modifiedFunDec.sbody.bstmts <- - (mkStmtOneInstr (Set((Var(v), NoOffset), zero, v.vdecl))) :: modifiedFunDec.sbody.bstmts; + (mkStmtOneInstr (Set((Var(v), NoOffset), zero, v.vdecl, v.vdecl))) :: modifiedFunDec.sbody.bstmts; ChangeTo(modifiedFunDec) end (* class monAllocaFunVisitor *) diff --git a/tools/lang/c/trapptrwrites/trapptrwrites.ml b/tools/lang/c/trapptrwrites/trapptrwrites.ml index 05d901a3..8c882e41 100644 --- a/tools/lang/c/trapptrwrites/trapptrwrites.ml +++ b/tools/lang/c/trapptrwrites/trapptrwrites.ml @@ -89,7 +89,7 @@ let trapPtrWrites file = match unrollType (typeOfLval lv) with | TPtr _ | TFun _ -> Call (None, Lval (var notifyPtrWriteFun), - [ mkCast (mkAddrOf lv) constVoidPtrPtrType ; Lval rv ], loc) :: tail + [ mkCast (mkAddrOf lv) constVoidPtrPtrType ; Lval rv ], loc, loc) :: tail | TComp (c, _) -> (* treat unions as structs, might not be a good idea... *) List.fold_left (fun acc field -> let flv = addOffsetLval (Field(field, NoOffset)) lv in @@ -101,31 +101,31 @@ let trapPtrWrites file = Call (None, Lval (var notifyCopyFun), [ mkAddrOf lv ; StartOf rv ; BinOp (Mult, length_exp, SizeOf eltyp, !upointType) ], - loc) :: tail + loc, loc) :: tail | _ -> tail in match i with - | Set (lv, _, _) | Call (Some lv, _, _, _) when not (lvNeedTrapCalls lv) -> + | Set (lv, _, _, _) | Call (Some lv, _, _, _, _) when not (lvNeedTrapCalls lv) -> SkipChildren - | Set(lv, Lval rv, l) -> - ChangeTo (addTrapCallsForLval lv rv l [Set(lv, Lval rv, l)]) - | Set(lv, e, l) -> + | Set(lv, Lval rv, l, _) -> + ChangeTo (addTrapCallsForLval lv rv l [Set(lv, Lval rv, l, l)]) + | Set(lv, e, l, _) -> let curFunc = match curFunc with | Some f -> f | None -> assert false in let tmpvar = var (makeTempVar curFunc (typeOfLval lv)) in - ChangeTo (Set(tmpvar, e, l) :: - addTrapCallsForLval lv tmpvar l [Set(lv, Lval tmpvar, l)]) - | Call(Some lv, f, args, l) -> + ChangeTo (Set(tmpvar, e, l, l) :: + addTrapCallsForLval lv tmpvar l [Set(lv, Lval tmpvar, l, l)]) + | Call(Some lv, f, args, l, _) -> let curFunc = match curFunc with | Some f -> f | None -> assert false in let tmpvar = var (makeTempVar curFunc (typeOfLval lv)) in - ChangeTo (Call(Some tmpvar, f, args, l) :: - addTrapCallsForLval lv tmpvar l [Set(lv, Lval tmpvar, l)]) + ChangeTo (Call(Some tmpvar, f, args, l, l) :: + addTrapCallsForLval lv tmpvar l [Set(lv, Lval tmpvar, l, l)]) | _ -> SkipChildren end in From 29d10490ddb2327c485f2f4e11bd463930270226 Mon Sep 17 00:00:00 2001 From: Tom Wallis Date: Tue, 16 Dec 2025 10:41:59 +0000 Subject: [PATCH 3/7] More-or-less building liballocs with goblint/cil --- .gitmodules | 15 ++++++++++ README.md | 6 ++-- contrib/Makefile | 53 ++++++++++++++++++++++++++++----- contrib/cil | 2 +- contrib/cppo | 1 + contrib/csexp | 1 + contrib/dune | 1 + contrib/yojson | 1 + include/liballocs_cil_inlines.h | 52 ++++++++++++++++---------------- tools/lang/c/bin/allocscc | 8 ++--- 10 files changed, 97 insertions(+), 43 deletions(-) create mode 160000 contrib/cppo create mode 160000 contrib/csexp create mode 160000 contrib/dune create mode 160000 contrib/yojson diff --git a/.gitmodules b/.gitmodules index 240bffc8..98138196 100644 --- a/.gitmodules +++ b/.gitmodules @@ -19,3 +19,18 @@ [submodule "contrib/elftin"] path = contrib/elftin url = https://github.com/stephenrkell/elftin.git +[submodule "contrib/yojson"] + path = contrib/yojson + url = https://github.com/ocaml-community/yojson.git +[submodule "contrib/dune"] + path = contrib/dune + url = https:/github.com/ocaml/dune +[submodule "contrib/cppo"] + path = contrib/cppo + url = https://github.com/ocaml-community/cppo.git +[submodule "contrib/csexp"] + path = contrib/csexp + url = https://github.com/ocaml-dune/csexp.git +[submodule "contrib/cil"] + path = contrib/cil + url = https://github.com/probablytom/cil.git diff --git a/README.md b/README.md index 397b4b34..3e65b4ba 100644 --- a/README.md +++ b/README.md @@ -220,11 +220,13 @@ look something like the following. $ sudo apt-get install libelf-dev libdw-dev binutils-dev \ autoconf automake libtool pkg-config autoconf-archive \ - g++ ocaml ocamlbuild ocaml-findlib \ + g++ ocaml ocamlbuild ocaml-dune ocaml-findlib \ + libppx-deriving-yojson-caml-dev \ default-jre-headless python3 python \ make git gawk gdb wget \ libunwind-dev libc6-dev-i386 zlib1g-dev libc6-dbg \ - libboost-{iostreams,regex,serialization,filesystem}-dev && \ + libboost-{iostreams,regex,serialization,filesystem}-dev + linux-libc-dev-i386-cross libdune-ocaml-dev && \ git clone https://github.com/stephenrkell/liballocs.git && \ cd liballocs && \ git submodule update --init --recursive && \ diff --git a/contrib/Makefile b/contrib/Makefile index 0e231315..71240110 100644 --- a/contrib/Makefile +++ b/contrib/Makefile @@ -1,6 +1,12 @@ THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST))) CONTRIB := $(realpath $(dir $(THIS_MAKEFILE))) +export OCAMLLIB := /usr/lib/ocaml/ +export PATH := ${PATH}:${OCAMLLIB}bin/ + +export CIL_CC=clang-18 +export CC=${CIL_CC} + # NOTE all this env.sh amounts to just a different way to do # ./configure --with-blah=/path/to/blah ? # ... but we prefer it because it's more compositional: @@ -121,21 +127,52 @@ clean:: # ----------------------------cil .PHONY: build-cil -build-cil: cil.stamp +build-cil: cil.stamp mainFeature.cmx + +.PHONY: yojson +yojson: + cd yojson && dune build -p yojson && dune install -p yojson --prefix=${OCAMLLIB} --libdir=${OCAMLLIB} + +.PHONY: csexp +csexp: + cd csexp && dune build -p csexp && dune install -p csexp --prefix=${OCAMLLIB} --libdir=${OCAMLLIB} + +.PHONY: cppo +cppo: + cd cppo && dune build -p cppo && dune install -p cppo --prefix=${OCAMLLIB} --libdir=${OCAMLLIB} + +.PHONY: dune-configurator +dune-configurator: csexp + cd dune && dune build -p dune-configurator && dune install -p dune-configurator --prefix=${OCAMLLIB} --libdir=${OCAMLLIB} # PROBLEM: cil's ocamlbuild takes a significant time to re-run even in the # case where nothing's changed. So use a stamp to run around that. -cil.stamp: cil/Makefile $(shell find cil -name '*.c' -o -name '*.ml' -o -name '*.mli' -o -name '*.in' -o -name '*.mly' ) - $(MAKE) -C cil all install-local && touch $@ -cil/Makefile: cil/configure - cd cil && CC=$${ALLOCSCC_CC:-$${CC:-cc}} ./configure INSTALL="`which install` -p" +cil.stamp: goblint-cil +goblint-cil: yojson cppo dune-configurator + cd cil && dune build && dune build @install && dune install --prefix=${OCAMLLIB} --libdir=${OCAMLLIB} + touch cil.stamp + +CONFIG_MK += \nCIL_ROOT ?= $(CONTRIB)/cil/\n +varlist += CIL_ROOT +export CIL_ROOT -CONFIG_MK += \nCIL_INSTALL ?= $(CONTRIB)/cil/lib\n +CONFIG_MK += \nCIL_INSTALL ?= $(CONTRIB)/cil/_build/install/default/lib/goblint-cil/\n varlist += CIL_INSTALL export CIL_INSTALL +.PHONY: mainFeature.cmx +mainFeature.cmx: + cd cil && cp ${CIL_ROOT}/src/mainFeature.ml ${CIL_ROOT}/src/mainFeature.mli ${CIL_INSTALL} && ocamlfind ocamlopt -c ${CIL_INSTALL}/mainFeature.mli && ocamlfind ocamlopt -linkpkg -package dynlink -package findlib -package str -package zarith -I ${CIL_INSTALL} ${CIL_INSTALL}goblintCil.cmxa ${CIL_INSTALL}mainFeature.ml + +.PHONY: goblint-cil-deps +goblint-cil-deps: cppo csexp dune-configurator yojson + clean:: - $(MAKE) -C cil clean + cd cil && dune clean + cd yojson && dune uninstall -p yojson --prefix=/usr/lib/ocaml/ + cd csexp && dune uninstall -p csexp --prefix=/usr/lib/ocaml/ + cd cppo && dune uninstall -p cppo --prefix=/usr/lib/ocaml/ + cd dune && dune uninstall -p dune-configurator --prefix=/usr/lib/ocaml/ rm -f cil.stamp # ----------------------------toolsub @@ -143,7 +180,7 @@ clean:: .PHONY: build-toolsub build-toolsub: build-cil $(MAKE) -C toolsub wrapper-recursive cilpp-recursive # don't build clang-based cccppp - $(MAKE) -C toolsub/wrapper/example/constructor-priority-checker dumpconstr + #$(MAKE) -C toolsub/wrapper/example/constructor-priority-checker dumpconstr CONFIG_MK += \nTOOLSUB ?= $(CONTRIB)/toolsub\n varlist += TOOLSUB diff --git a/contrib/cil b/contrib/cil index 46078e18..6304bfd5 160000 --- a/contrib/cil +++ b/contrib/cil @@ -1 +1 @@ -Subproject commit 46078e18e855498043d757781b2d3fbf1ea7c514 +Subproject commit 6304bfd580b086a391a7455fb9ed35152b4addd4 diff --git a/contrib/cppo b/contrib/cppo new file mode 160000 index 00000000..33f30cdd --- /dev/null +++ b/contrib/cppo @@ -0,0 +1 @@ +Subproject commit 33f30cdd68a8c385c64ed17f1cf883a7a893608d diff --git a/contrib/csexp b/contrib/csexp new file mode 160000 index 00000000..07eb8988 --- /dev/null +++ b/contrib/csexp @@ -0,0 +1 @@ +Subproject commit 07eb8988452ad51a09d0ab7379d73a87674aba6e diff --git a/contrib/dune b/contrib/dune new file mode 160000 index 00000000..ef3b45c0 --- /dev/null +++ b/contrib/dune @@ -0,0 +1 @@ +Subproject commit ef3b45c08a4db30a2581f231ccc267ec4ce73c3c diff --git a/contrib/yojson b/contrib/yojson new file mode 160000 index 00000000..d692c15d --- /dev/null +++ b/contrib/yojson @@ -0,0 +1 @@ +Subproject commit d692c15dc630a1a1635719b5426299df6f02c5ef diff --git a/include/liballocs_cil_inlines.h b/include/liballocs_cil_inlines.h index dc60af1d..b173bdf5 100644 --- a/include/liballocs_cil_inlines.h +++ b/include/liballocs_cil_inlines.h @@ -85,15 +85,15 @@ CURRENT_ALLOC_VARS_QUALIFIERS void *__current_allocsite CURRENT_ALLOC_VARS_QUALI void __liballocs_unindex_stack_objects_counted_by(unsigned long *, void *frame_addr); -extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_alloca_caller_frame_cleanup)(void *counter); -extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_alloca_caller_frame_cleanup)(void *counter) +extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_alloca_caller_frame_cleanup)(void *counter); +extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_alloca_caller_frame_cleanup)(void *counter) { __liballocs_unindex_stack_objects_counted_by((unsigned long *) counter, __builtin_frame_address(0)); } /* alloca helpers */ -extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_sp)(void); -extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_sp)(void) +extern inline const void *(__attribute__((always_inline,gnu_inline)) __liballocs_get_sp)(void); +extern inline const void *(__attribute__((always_inline,gnu_inline)) __liballocs_get_sp)(void) { unsigned long our_sp; #ifdef UNW_TARGET_X86 @@ -104,8 +104,8 @@ extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liba return (const void*) our_sp; } -extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_bp)(void); -extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_bp)(void) +extern inline const void *(__attribute__((always_inline,gnu_inline)) __liballocs_get_bp)(void); +extern inline const void *(__attribute__((always_inline,gnu_inline)) __liballocs_get_bp)(void) { return (const void *) __builtin_frame_address(0); } @@ -118,8 +118,8 @@ extern inline const void *(__attribute__((always_inline,gnu_inline,used)) __liba * for the allocation site / type metadata. We call a helper to get * the *overall* size, and then the __liballocs_notify_and_adjust_alloca() * function will fill in both the header and the trailer. */ -extern inline unsigned long (__attribute__((always_inline,gnu_inline,used)) __liballocs_alloca_size)(unsigned long orig_size); -extern inline unsigned long (__attribute__((always_inline,gnu_inline,used)) __liballocs_alloca_size)(unsigned long orig_size) +extern inline unsigned long (__attribute__((always_inline,gnu_inline)) __liballocs_alloca_size)(unsigned long orig_size); +extern inline unsigned long (__attribute__((always_inline,gnu_inline)) __liballocs_alloca_size)(unsigned long orig_size) { /* Insert heap trailer etc.. * Basically we have to do everything that our malloc hooks, allocator wrappers @@ -138,8 +138,8 @@ extern inline unsigned long (__attribute__((always_inline,gnu_inline,used)) __li * we don't track them. */ } -extern inline void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_notify_and_adjust_alloca)(void *allocated, unsigned long orig_size, unsigned long tweaked_size, unsigned long *frame_counter, void *caller); -extern inline void *(__attribute__((always_inline,gnu_inline,used)) __liballocs_notify_and_adjust_alloca)(void *allocated, unsigned long orig_size, unsigned long tweaked_size, unsigned long *frame_counter, void *caller) +extern inline void *(__attribute__((always_inline,gnu_inline)) __liballocs_notify_and_adjust_alloca)(void *allocated, unsigned long orig_size, unsigned long tweaked_size, unsigned long *frame_counter, void *caller); +extern inline void *(__attribute__((always_inline,gnu_inline)) __liballocs_notify_and_adjust_alloca)(void *allocated, unsigned long orig_size, unsigned long tweaked_size, unsigned long *frame_counter, void *caller) { #ifndef LIBALLOCS_NO_ZERO __builtin_memset(allocated, 0, tweaked_size); @@ -213,8 +213,8 @@ struct __liballocs_memrange_cache }; extern struct __liballocs_memrange_cache /* __thread */ __liballocs_ool_cache; -extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_check_cache_sanity )(struct __liballocs_memrange_cache *cache __attribute__((unused))); -extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_check_cache_sanity )(struct __liballocs_memrange_cache *cache __attribute__((unused))) +extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_check_cache_sanity )(struct __liballocs_memrange_cache *cache __attribute__((unused))); +extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_check_cache_sanity )(struct __liballocs_memrange_cache *cache __attribute__((unused))) { #ifdef DEBUG unsigned visited_linear = 0u; @@ -247,8 +247,8 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c #endif } -extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_unlink )(struct __liballocs_memrange_cache *cache, unsigned i); -extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_unlink )(struct __liballocs_memrange_cache *cache, unsigned i) +extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_unlink )(struct __liballocs_memrange_cache *cache, unsigned i); +extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_unlink )(struct __liballocs_memrange_cache *cache, unsigned i) { __liballocs_check_cache_sanity(cache); /* unset validity and make this the next victim */ @@ -266,8 +266,8 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c __liballocs_check_cache_sanity(cache); } -extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_push_head_mru )(struct __liballocs_memrange_cache *cache, unsigned i); -extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_push_head_mru )(struct __liballocs_memrange_cache *cache, unsigned i) +extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_push_head_mru )(struct __liballocs_memrange_cache *cache, unsigned i); +extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_push_head_mru )(struct __liballocs_memrange_cache *cache, unsigned i) { __liballocs_check_cache_sanity(cache); /* Put us at the head of the LRU chain. */ @@ -284,8 +284,8 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c __liballocs_check_cache_sanity(cache); } -extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_bump_victim )(struct __liballocs_memrange_cache *cache, unsigned i); -extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_bump_victim )(struct __liballocs_memrange_cache *cache, unsigned i) +extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_bump_victim )(struct __liballocs_memrange_cache *cache, unsigned i); +extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_bump_victim )(struct __liballocs_memrange_cache *cache, unsigned i) { __liballocs_check_cache_sanity(cache); /* make sure we're not the next victim */ @@ -299,8 +299,8 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c __liballocs_check_cache_sanity(cache); } -extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_bump_mru )(struct __liballocs_memrange_cache *cache, unsigned i); -extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_cache_bump_mru )(struct __liballocs_memrange_cache *cache, unsigned i) +extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_bump_mru )(struct __liballocs_memrange_cache *cache, unsigned i); +extern inline void (__attribute__((always_inline,gnu_inline)) __liballocs_cache_bump_mru )(struct __liballocs_memrange_cache *cache, unsigned i) { __liballocs_check_cache_sanity(cache); if (cache->head_mru != i) @@ -312,10 +312,10 @@ extern inline void (__attribute__((always_inline,gnu_inline,used)) __liballocs_c } extern inline -struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline,used)) +struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline)) __liballocs_memrange_cache_lookup )(struct __liballocs_memrange_cache *cache, const void *obj, struct uniqtype *t, unsigned long require_period); extern inline -struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline,used)) +struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline)) __liballocs_memrange_cache_lookup )(struct __liballocs_memrange_cache *cache, const void *obj, struct uniqtype *t, unsigned long require_period) { #ifndef LIBALLOCS_NOOP_INLINES @@ -352,10 +352,10 @@ __liballocs_memrange_cache_lookup )(struct __liballocs_memrange_cache *cache, co } extern inline -struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline,used)) +struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline)) __liballocs_memrange_cache_lookup_notype )(struct __liballocs_memrange_cache *cache, const void *obj, unsigned long require_period); extern inline -struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline,used)) +struct __liballocs_memrange_cache_entry_s *(__attribute__((always_inline,gnu_inline)) __liballocs_memrange_cache_lookup_notype )(struct __liballocs_memrange_cache *cache, const void *obj, unsigned long require_period) { #ifndef LIBALLOCS_NOOP_INLINES @@ -389,8 +389,8 @@ __liballocs_memrange_cache_lookup_notype )(struct __liballocs_memrange_cache *ca return (struct __liballocs_memrange_cache_entry_s *)(void*)0; } -extern inline struct uniqtype *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_cached_object_type)(const void *addr); -extern inline struct uniqtype *(__attribute__((always_inline,gnu_inline,used)) __liballocs_get_cached_object_type)(const void *addr) +extern inline struct uniqtype *(__attribute__((always_inline,gnu_inline)) __liballocs_get_cached_object_type)(const void *addr); +extern inline struct uniqtype *(__attribute__((always_inline,gnu_inline)) __liballocs_get_cached_object_type)(const void *addr) { struct __liballocs_memrange_cache_entry_s *found = __liballocs_memrange_cache_lookup_notype( &__liballocs_ool_cache, diff --git a/tools/lang/c/bin/allocscc b/tools/lang/c/bin/allocscc index 2ded7e16..8c8b7d2e 100755 --- a/tools/lang/c/bin/allocscc +++ b/tools/lang/c/bin/allocscc @@ -13,14 +13,10 @@ REAL_FILE = os.path.realpath(__file__) REAL_DIR = os.path.realpath(os.path.dirname(REAL_FILE)) liballocs_base = os.path.realpath(REAL_DIR + "/../../../..") cil_base = os.environ.get("CIL_ROOT", liballocs_base + "/contrib/cil/") +cilly_cmd = cil_base + "/_build/install/default/bin/cilly" sys.path.append(liballocs_base + "/tools") from allocscompilerwrapper import * -existing_cil_install = os.environ.get("CIL_INSTALL") -if cil_base == None: - cilly_cmd = liballocs_base + "/_build/install/default/bin/cilly" - existing_cil_install = liballocs_base + "/contrib/cil/_build/install/default/lib/goblint-cil/" -else: - cilly_cmd = cil_base + "/_build/install/default/bin/cilly" +existing_cil_install = os.environ.get("CIL_INSTALL", cil_base + "_build/install/default/lib/goblint-cil") existing_elftin = os.environ.get("ELFTIN") if existing_elftin == None: os.putenv("ELFTIN", liballocs_base + "/contrib/elftin") From bd10eb2b2af232450bcae5be19395034980fcace Mon Sep 17 00:00:00 2001 From: Tom Wallis Date: Thu, 18 Dec 2025 15:51:27 +0000 Subject: [PATCH 4/7] Install cil+configurator to `lib/ocaml`, remove manual deps --- .gitignore | 2 ++ .gitmodules | 11 +---------- README.md | 7 +++++-- contrib/Makefile | 26 +++++++------------------- contrib/cppo | 1 - contrib/csexp | 1 - contrib/yojson | 1 - 7 files changed, 15 insertions(+), 34 deletions(-) delete mode 160000 contrib/cppo delete mode 160000 contrib/csexp delete mode 160000 contrib/yojson diff --git a/.gitignore b/.gitignore index 9dff4a8a..37a2de4c 100644 --- a/.gitignore +++ b/.gitignore @@ -196,3 +196,5 @@ oopsla*.ps *.orig /tests/bit-fields/bit-fields /tests/packed-seq-walk/packed-seq-walk + +/lib/ocaml diff --git a/.gitmodules b/.gitmodules index 98138196..e6d88c38 100644 --- a/.gitmodules +++ b/.gitmodules @@ -19,18 +19,9 @@ [submodule "contrib/elftin"] path = contrib/elftin url = https://github.com/stephenrkell/elftin.git -[submodule "contrib/yojson"] - path = contrib/yojson - url = https://github.com/ocaml-community/yojson.git [submodule "contrib/dune"] path = contrib/dune - url = https:/github.com/ocaml/dune -[submodule "contrib/cppo"] - path = contrib/cppo - url = https://github.com/ocaml-community/cppo.git -[submodule "contrib/csexp"] - path = contrib/csexp - url = https://github.com/ocaml-dune/csexp.git + url = git@github.com:probablytom/dune [submodule "contrib/cil"] path = contrib/cil url = https://github.com/probablytom/cil.git diff --git a/README.md b/README.md index 3e65b4ba..1fa1570e 100644 --- a/README.md +++ b/README.md @@ -221,11 +221,14 @@ look something like the following. $ sudo apt-get install libelf-dev libdw-dev binutils-dev \ autoconf automake libtool pkg-config autoconf-archive \ g++ ocaml ocamlbuild ocaml-dune ocaml-findlib \ - libppx-deriving-yojson-caml-dev \ + libppx-deriving-yojson-ocaml-dev \ default-jre-headless python3 python \ make git gawk gdb wget \ libunwind-dev libc6-dev-i386 zlib1g-dev libc6-dbg \ - libboost-{iostreams,regex,serialization,filesystem}-dev + libboost-{iostreams,regex,serialization,filesystem}-dev \ + cppo libcsexp-ocaml libcsexp-ocaml-dev libyojson-ocaml \ + libyojson-ocaml-dev libnum-ocaml libnum-ocaml-dev \ + libzarith-ocaml libzarith-ocaml-dev \ linux-libc-dev-i386-cross libdune-ocaml-dev && \ git clone https://github.com/stephenrkell/liballocs.git && \ cd liballocs && \ diff --git a/contrib/Makefile b/contrib/Makefile index 71240110..12ce3d29 100644 --- a/contrib/Makefile +++ b/contrib/Makefile @@ -1,8 +1,8 @@ THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST))) CONTRIB := $(realpath $(dir $(THIS_MAKEFILE))) -export OCAMLLIB := /usr/lib/ocaml/ -export PATH := ${PATH}:${OCAMLLIB}bin/ +export OCAML_LIBDEST := ${CONTRIB}/../lib/ocaml/ +export PATH := ${PATH}:${OCAML_LIBDEST}bin/ export CIL_CC=clang-18 export CC=${CIL_CC} @@ -129,34 +129,22 @@ clean:: .PHONY: build-cil build-cil: cil.stamp mainFeature.cmx -.PHONY: yojson -yojson: - cd yojson && dune build -p yojson && dune install -p yojson --prefix=${OCAMLLIB} --libdir=${OCAMLLIB} - -.PHONY: csexp -csexp: - cd csexp && dune build -p csexp && dune install -p csexp --prefix=${OCAMLLIB} --libdir=${OCAMLLIB} - -.PHONY: cppo -cppo: - cd cppo && dune build -p cppo && dune install -p cppo --prefix=${OCAMLLIB} --libdir=${OCAMLLIB} - .PHONY: dune-configurator -dune-configurator: csexp - cd dune && dune build -p dune-configurator && dune install -p dune-configurator --prefix=${OCAMLLIB} --libdir=${OCAMLLIB} +dune-configurator: + cd dune && dune build -p dune-configurator && dune install -p dune-configurator --prefix=${OCAML_LIBDEST} --libdir=${OCAML_LIBDEST} # PROBLEM: cil's ocamlbuild takes a significant time to re-run even in the # case where nothing's changed. So use a stamp to run around that. cil.stamp: goblint-cil -goblint-cil: yojson cppo dune-configurator - cd cil && dune build && dune build @install && dune install --prefix=${OCAMLLIB} --libdir=${OCAMLLIB} +goblint-cil: dune-configurator + cd cil && dune build && dune build @install && dune install --prefix=${OCAML_LIBDEST} --libdir=${OCAML_LIBDEST} touch cil.stamp CONFIG_MK += \nCIL_ROOT ?= $(CONTRIB)/cil/\n varlist += CIL_ROOT export CIL_ROOT -CONFIG_MK += \nCIL_INSTALL ?= $(CONTRIB)/cil/_build/install/default/lib/goblint-cil/\n +CONFIG_MK += \nCIL_INSTALL ?= $(CONTRIB)/../lib/ocaml/goblint-cil/\n varlist += CIL_INSTALL export CIL_INSTALL diff --git a/contrib/cppo b/contrib/cppo deleted file mode 160000 index 33f30cdd..00000000 --- a/contrib/cppo +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 33f30cdd68a8c385c64ed17f1cf883a7a893608d diff --git a/contrib/csexp b/contrib/csexp deleted file mode 160000 index 07eb8988..00000000 --- a/contrib/csexp +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 07eb8988452ad51a09d0ab7379d73a87674aba6e diff --git a/contrib/yojson b/contrib/yojson deleted file mode 160000 index d692c15d..00000000 --- a/contrib/yojson +++ /dev/null @@ -1 +0,0 @@ -Subproject commit d692c15dc630a1a1635719b5426299df6f02c5ef From 3afcf2b874ebf5786457ef6125936fcc7c16188a Mon Sep 17 00:00:00 2001 From: Tom Wallis Date: Fri, 19 Dec 2025 16:35:24 +0000 Subject: [PATCH 5/7] Clean up clang-18 reference from Makefile (CC is gcc unless CIL_CC set) --- contrib/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/contrib/Makefile b/contrib/Makefile index b08d3070..eaf74e9e 100644 --- a/contrib/Makefile +++ b/contrib/Makefile @@ -4,8 +4,8 @@ CONTRIB := $(realpath $(dir $(THIS_MAKEFILE))) export OCAML_LIBDEST := ${CONTRIB}/../lib/ocaml/ export PATH := ${PATH}:${OCAML_LIBDEST}bin/ -export CIL_CC=clang-18 -export CC=${CIL_CC} +export CIL_CC := gcc +export CC := ${CIL_CC} # NOTE all this env.sh amounts to just a different way to do # ./configure --with-blah=/path/to/blah ? From ebedd2212d64b9d591c7c84445133f4e39a31e3a Mon Sep 17 00:00:00 2001 From: Tom Wallis Date: Fri, 19 Dec 2025 16:42:20 +0000 Subject: [PATCH 6/7] Update apt dependencies for circleCI --- .circleci/config.yml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.circleci/config.yml b/.circleci/config.yml index 3fbb4803..118c54ce 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -16,6 +16,11 @@ jobs: ocaml ocamlbuild ocaml-findlib libnum-ocaml-dev \ default-jdk-headless python3 \ make git gawk gdb wget libc6-dbg \ + ocaml-dune libdune-ocaml-dev \ + libyojson-ocaml libyojson-ocaml-dev libppx-deriving-yojson-ocaml-dev \ + libzarith-ocaml libzarith-ocaml-dev \ + libnum-ocaml libnum-ocaml-dev \ + libcsexp-ocaml libcsexp-ocaml-dev \ libunwind-dev libunwind-dev:i386 linux-libc-dev-i386-cross libc6-dev-i386 \ libboost-iostreams-dev libboost-regex-dev \ libboost-serialization-dev libboost-filesystem-dev libffi-dev \ From fc8d5e8f68476a55b098950c3c022bf4a789eed7 Mon Sep 17 00:00:00 2001 From: Tom Wallis Date: Fri, 19 Dec 2025 17:03:01 +0000 Subject: [PATCH 7/7] .gitignore changes to ensure lib/ocaml exists --- .gitignore | 2 -- lib/ocaml/.gitignore | 8 ++++++++ 2 files changed, 8 insertions(+), 2 deletions(-) create mode 100644 lib/ocaml/.gitignore diff --git a/.gitignore b/.gitignore index 37a2de4c..9dff4a8a 100644 --- a/.gitignore +++ b/.gitignore @@ -196,5 +196,3 @@ oopsla*.ps *.orig /tests/bit-fields/bit-fields /tests/packed-seq-walk/packed-seq-walk - -/lib/ocaml diff --git a/lib/ocaml/.gitignore b/lib/ocaml/.gitignore new file mode 100644 index 00000000..83f42c9b --- /dev/null +++ b/lib/ocaml/.gitignore @@ -0,0 +1,8 @@ +# We want to ensure lib/ocaml _always_ exists, but we can't commit an empty dir +# to a git repo. There has to be some content at this path. However, everything +# that gets placed here is a build artifact that shouldn't be committed. + +# So: ignore everything in this directory _except_ this file, so that this file +# ensures the path exists. +* +!.gitignore