From bec181d0cec53f427c04f8ce92f0a05172a9a86b Mon Sep 17 00:00:00 2001 From: Ben Karel Date: Fri, 2 May 2025 16:12:18 -0400 Subject: [PATCH 1/4] Standardize on using dune to build CodeHawk Remove the Shake-based build (even though it's a great example!). --- .gitignore | 3 + CodeHawk/README.md | 168 +++------------ CodeHawk/Shakefile.hs | 387 ---------------------------------- CodeHawk/non_file_modules.txt | 90 -------- newfile | 0 5 files changed, 27 insertions(+), 621 deletions(-) delete mode 100644 CodeHawk/Shakefile.hs delete mode 100644 CodeHawk/non_file_modules.txt delete mode 100644 newfile diff --git a/.gitignore b/.gitignore index 16ab0ff9..94cc57d2 100644 --- a/.gitignore +++ b/.gitignore @@ -11,6 +11,9 @@ # ocamlbuild working directory _build/ +# local opam switch +_opam/ + # ocamlbuild targets *.byte *.native diff --git a/CodeHawk/README.md b/CodeHawk/README.md index 781c3b3d..ce91359e 100644 --- a/CodeHawk/README.md +++ b/CodeHawk/README.md @@ -8,166 +8,46 @@ Building codehawk requires the following applications and libraries: - The Findlib / ocamlfind library manager - The Zlib C library, version 1.1.3 or up - The Zarith library +- goblint-cil, version 2.0.6 The CodeHawk Tool Suite contains three analyzers that can all be built individually. All three analyzers have an optional gui that can be built separately (and that requires additional dependencies to be installed). +The gui is current out-of-date and will require additional work to revive. -### Install dependencies: Ubuntu 16.04 or later (without gui) +### Install Dependencies: -``` -sudo apt update -y -sudo apt install software-properties-common pkg-config m4 zlib1g-dev libgmp-dev -y -sudo add-apt-repository ppa:avsm/ppa -y -sudo apt update -y -sudo apt install opam -git clone https://github.com/static-analysis-engineering/codehawk.git -opam init --bare --no-setup --disable-sandboxing -opam switch create codehawk-4.12.1 4.12.1 --no-switch -eval $(opam env --switch=codehawk-4.12.1 --set-switch) -opam install ocamlfind zarith camlzip extlib goblint-cil -cd codehawk/CodeHawk -``` - -Depending on which analyzer you want to build: -- **Binary:** `./make_binary_analyzer.sh` - - analyzer binary: CHB/bchcmdline/chx86_analyze -- **C:** `./make_c_analyzer.sh` - - parser binary: CHC/cchcil/parseFile - - analyzer binary: CHC/cchcmdline/canalyzer -- **Java:** `./make_java_analyzer.sh` - - analyzer binary: CHJ/jchstac/chj_initialize -- **all:** `./full_make_no_gui.sh` - - analyzer/parser binaries: all of the above - - -### Install dependencies and build: Ubuntu 16.04 or later (including gui) +These commands should work for Ubuntu 22.04+: ``` sudo apt update -y -sudo apt install software-properties-common pkg-config m4 zlib1g-dev libgmp-dev liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev -y -sudo add-apt-repository ppa:avsm/ppa -y -sudo apt update -y -sudo apt install opam -git clone https://github.com/static-analysis-engineering/codehawk.git -opam init --bare --no-setup --disable-sandboxing -opam switch create codehawk-4.12.1 4.12.1 --no-switch -eval $(opam env --switch=codehawk-4.12.1 --set-switch) -opam install ocamlfind zarith camlzip extlib lablgtk lablgtk-extras goblint-cil -cd codehawk/CodeHawk -./full_make.sh -``` - -# Building with shake - -### High-level process: - -1. Install dependencies -2. Install the shake build system -3. Install ocaml -4. Build CodeHawk - -The top-level dependencies needed to build CodeHawk are zlib for compression, the shake build -system, and the ocaml package manager (opam). In addition to the commands below, use the `opam` -setup above to get the dependencies. - -### Generic Unix - -Other dependencies: `pkg-config`, `m4` - -``` -sudo apt update -y -sudo apt install curl -y -curl -sSL https://get.haskellstack.org/ | sh -sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) -stack install shake -git clone https://github.com/static-analysis-engineering/codehawk.git -cd codehawk/CodeHawk -stack runghc Shakefile.hs -``` - -### Arch Linux - -``` -sudo pacman -Syu opam haskell-shake lablgtk2 -git clone https://github.com/static-analysis-engineering/codehawk.git -cd codehawk/CodeHawk -shake -``` - -### Fedora - -``` -sudo yum install opam shake ghc-compiler ghc-shake-devel diffutils zlib-devel ocaml-lablgtk-devel -y -git clone https://github.com/static-analysis-engineering/codehawk.git -cd codehawk/CodeHawk -shake -``` - -### Homebrew +sudo apt install --no-install-recommends software-properties-common \ + build-essential unzip \ + pkg-config m4 zlib1g-dev libgmp-dev bubblewrap -y -``` -brew install opam -brew install cabal-install -brew install lablgtk -cabal update -cabal install --lib shake -cabal install --lib unordered-containers -git clone https://github.com/static-analysis-engineering/codehawk.git -cd codehawk/CodeHawk -~/.cabal/bin/shake -``` +# Run with sudo if you wish to install globally +bash -c "sh <(curl -fsSL https://opam.ocaml.org/install.sh)" +opam init --bare -### MacPorts - -``` -sudo port install opam -sudo port install hs-cabal-install -sudo port install lablgtk2 -cabal update -cabal install --lib shake -cabal install --lib unordered-containers git clone https://github.com/static-analysis-engineering/codehawk.git cd codehawk/CodeHawk -~/.cabal/bin/shake +opam switch create . 5.2.0 && eval $(opam env) +opam install dune ocamlfind zarith camlzip extlib goblint-cil.2.0.6 ``` -### Ubuntu 19.04 or later, Debian Buster or later - -``` -sudo apt update -y -sudo apt install cabal-install pkg-config m4 zlib1g-dev opam liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev -y -cabal update -cabal install shake -git clone https://github.com/static-analysis-engineering/codehawk.git -cd codehawk/CodeHawk -~/.cabal/bin/shake -``` - -### Ubuntu 16.04 or later - -``` -sudo apt update -y -sudo apt install software-properties-common cabal-install pkg-config m4 zlib1g-dev liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev -y -sudo add-apt-repository ppa:avsm/ppa -y -sudo apt update -y -sudo apt install opam -cabal update -cabal install shake -git clone https://github.com/static-analysis-engineering/codehawk.git -cd codehawk/CodeHawk -~/.cabal/bin/shake -``` +Depending on which analyzer you want to build: +- **Binary:** `dune build CHB` +- **C:** `dune build CHC` +- **Java:** `dune build CHJ` +- **all:** `dune build` -### Manually configured opam +These targets can be combined, e.g. `dune build CHB CHC`. -Before the final "shake" command in one of the above instructions: +The Makefiles in the repository are to help CodeHawk's developers +debug circular module dependencies, they are not intended for users. -``` -opam init --bare --no-setup --disable-sandboxing -opam switch create codehawk-4.12.1 4.09.0 --no-switch -eval $(opam env --switch=codehawk-4.12.1 --set-switch) -opam install ocamlfind zarith camlzip extlib lablgtk lablgtk-extras -/path/to/shake -``` +Dependencies for other OS flavors: +- Arch Linux: `sudo pacman -Syu opam` +- Fedora: `sudo yum install opam diffutils zlib-devel ocaml-lablgtk-devel -y` +- macOS: `brew install opam` diff --git a/CodeHawk/Shakefile.hs b/CodeHawk/Shakefile.hs deleted file mode 100644 index 7e480b6c..00000000 --- a/CodeHawk/Shakefile.hs +++ /dev/null @@ -1,387 +0,0 @@ -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE TypeFamilies #-} - -import Control.Monad -import Development.Shake -import Development.Shake.Classes -import Development.Shake.Command -import Development.Shake.FilePath -import Development.Shake.Util -import Data.Char -import Data.List -import Data.HashSet (HashSet) -import qualified Data.HashSet as HashSet -import Data.Map (Map) -import qualified Data.Map as Map -import Data.Set (Set) -import qualified Data.Set as Set -import Data.Maybe -import System.Console.GetOpt -import System.IO.Unsafe -import System.Directory - -ignoredOriginalFiles :: [String] -> [String] -ignoredOriginalFiles inList = - let nonBuild = filter (\file -> not $ elem "_build" $ splitDirectories file) inList in - let nonparser = filter (\file -> not $ elem "chifparser" $ splitDirectories file) nonBuild in - nonparser - -moduleToFile :: String -> String -moduleToFile modul = - let firstChar : rest = modul in - (toLower firstChar) : rest - -fileToModule :: String -> String -fileToModule modul = - let firstChar : rest = modul in - (toUpper firstChar) : rest - -dropLibraryModules :: [String] -> [String] -> [String] -dropLibraryModules libraryModules modules = - let knownLibraryModules = HashSet.fromList libraryModules in - filter (\modul -> not $ HashSet.member modul knownLibraryModules) modules - -copyFileChangedWithAnnotation :: String -> String -> Action () -copyFileChangedWithAnnotation oldPath newPath = do - contents <- readFile' oldPath - let newContents = "# 1 \"" ++ oldPath ++ "\"\n" ++ contents - writeFileChanged newPath newContents - -data Flags = Warnings deriving Eq -flagDefs = [Option "" ["warnings"] (NoArg $ Right Warnings) "Fail on warnings"] - -main :: IO () -main = do - ver <- getHashedShakeVersion ["Shakefile.hs"] - let defaultShakeOptions = shakeOptions { - shakeFiles="_build", - shakeProgress = progressSimple, - shakeLint = Just LintBasic, - shakeVersion = ver, - shakeThreads = 0 -- Use the number of cpus - } - shakeArgsWith defaultShakeOptions flagDefs $ \flagValues targets -> return $ Just $ do - let rules = runBuild flagValues - if null targets then rules else want targets >> withoutActions rules - -newtype ModuleDependencies = ModuleDependencies String deriving (Show,Typeable,Eq,Hashable,Binary,NFData) -type instance RuleResult ModuleDependencies = [String] - -newtype NonFileModules = NonFileModules () deriving (Show,Typeable,Eq,Hashable,Binary,NFData) -type instance RuleResult NonFileModules = [String] - -newtype ExtraFlags = ExtraFlags () deriving (Show,Typeable,Eq,Hashable,Binary,NFData) -type instance RuleResult ExtraFlags = [String] - -ocamlfind_libraries = ["zarith", "extlib", "camlzip", "goblint-cil"] - -runBuild :: [Flags] -> Rules () -runBuild flags = do - - addOracle $ \(ExtraFlags _) -> do - return $ if Warnings `elem` flags then ["-warn-error", "A"] else [] - - originalToMap <- liftIO $ unsafeInterleaveIO $ do - mlis <- getDirectoryFilesIO "" ["CH//*.mli", "CHC//*.mli", "CHB//*.mli", "CHJ//*.mli", "CH_gui//*.mli", "CHT//*.mli"] - mls <- getDirectoryFilesIO "" ["CH//*.ml", "CHC//*.ml", "CHB//*.ml", "CHJ//*.ml", "CH_gui//*.ml", "CHT//*.ml"] - let inputs = ignoredOriginalFiles $ mlis ++ mls - let pairs = [(takeFileName file, file) | file <- inputs] - return $ Map.fromList pairs - - phony "clean" $ do - putNormal "Cleaning files in _bin, _build, _docs_private, _docs_public" - removeFilesAfter "_bin" ["//*"] - removeFilesAfter "_build" ["//*"] - removeFilesAfter "_odoc" ["//*"] - removeFilesAfter "_docs_private" ["//*"] - removeFilesAfter "_docs_public" ["//*"] - - "_build/*.mli" %> \out -> - case Map.lookup (dropDirectory1 out) originalToMap of - Just original -> copyFileChangedWithAnnotation original out - Nothing -> error $ "No file matching " ++ (dropDirectory1 out) - - getLibraryModules <- addOracle $ \NonFileModules{} -> do - file <- readFile' "non_file_modules.txt" - return $ lines file - - getModuleDeps <- addOracleCache $ \(ModuleDependencies file) -> do - need [file] - Stdout dependencies_str <- cmd "ocamldep -modules" file - let [(_, modules)] = parseMakefile dependencies_str - libraryModules <- getLibraryModules $ NonFileModules () - return $ dropLibraryModules libraryModules modules - - let documentDir directory = do - "_build" takeBaseName directory -<.> "mld" %> \out -> do - mlis_full_path <- getDirectoryFiles directory ["*.mli"] - let children = unwords [takeBaseName mli | mli <- mlis_full_path] - let contents = "{0 " ++ takeBaseName directory ++ "}\n\n{!modules: " ++ children ++ "}" - writeFileChanged out contents - - "_build" "page-" ++ takeBaseName directory -<.> "odoc" %> \out -> do - need ["_build/page-_odoc.odoc"] - need ["_build" takeBaseName directory -<.> "mld"] - mlis_full_path <- getDirectoryFiles directory ["*.mli"] - let children = ["--child=" ++ takeBaseName mli | mli <- mlis_full_path] - cmd_ (Cwd "_build") "odoc compile" (takeBaseName directory -<.> "mld") children "-I . --parent=_odoc" - - "_build" "page-" ++ takeBaseName directory -<.> "odocl" %> \out -> do - need [out -<.> "odoc"] - need ["_build" takeBaseName directory -<.> "mld"] - mlis_full_path <- getDirectoryFiles directory ["*.mli"] - need ["_build" takeBaseName mli -<.> "odoc" | mli <- mlis_full_path] - cmd_ (Cwd "_build") "odoc link" ("page-" ++ takeBaseName directory -<.> "odoc") "-I ." - - "_odoc" takeBaseName directory "index.html" %> \out -> do - let odocl = "_build" "page-" ++ takeBaseName directory -<.> "odocl" - need [odocl] - mlis_full_path <- getDirectoryFiles directory ["*.mli"] - need ["_odoc" takeBaseName directory fileToModule (takeBaseName mli) "index.html" | mli <- mlis_full_path] - cmd_ "odoc html-generate" odocl "--output-dir . --support-uri=_odoc --theme-uri=_odoc" - - "_odoc" "*" "*" "index.html" %> \out -> do - let modul = moduleToFile $ takeBaseName $ takeDirectory out - let odocl = "_build" modul -<.> "odocl" - need [odocl] - cmd_ "odoc html-generate" odocl "--output-dir . --support-uri=_odoc --theme-uri=_odoc" - - let docDirectories = [ - "CH/xprlib", - "CH/chutil", - "CH/chlib", - "CHB/bchlib", - "CHB/bchlibx86", - "CHB/bchlibpower32", - "CHB/bchcil", - "CHB/bchlibarm32", - "CHB/bchlibpe", - "CHB/bchlibmips32", - "CHB/bchanalyze", - "CHB/bchcmdline", - "CHB/bchlibelf", - "CHC/cchcmdline", - "CHC/cchlib", - "CHC/cchcil", - "CHC/cchpre", - "CHC/cchanalyze", - "CHJ/jchpre", - "CHJ/jchmuse", - "CHJ/jchstac", - "CHJ/jchlib", - "CHJ/jchpoly", - "CHJ/jchcost", - "CHJ/jchfeatures", - "CHJ/jchsys", - "CHT/tchlib", - "CHT/CH_tests/xprlib_tests/txprlib", - "CHT/CH_tests/xprlib_tests/txxprlib", - "CHT/CHB_tests/bchlib_tests/tbchlib", - "CHT/CHB_tests/bchlib_tests/txbchlib", - "CHT/CHB_tests/bchlibelf_tests/tbchlibelf", - "CHT/CHB_tests/bchlibelf_tests/txbchlibelf", - "CHT/CHB_tests/bchlibarm32_tests/tbchlibarm32", - "CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32", - "CHT/CHB_tests/bchlibpower32_tests/txbchlibpower32" - ] - forM_ docDirectories documentDir - - "_build" "_odoc.mld" %> \out -> do - let children = intercalate "\n" ["- {!page-" ++ takeBaseName dir ++ "}" | dir <- docDirectories] - let contents = "{0 CodeHawk}\n\n" ++ children - writeFileChanged out contents - - "_build" "page-_odoc.odoc" %> \out -> do - need ["_build/_odoc.mld"] - let children = ["--child=" ++ takeBaseName dir | dir <- docDirectories] - cmd_ (Cwd "_build") "odoc compile _odoc.mld" children "-I ." - - "_build" "page-_odoc.odocl" %> \out -> do - need ["_build/page-_odoc.odoc"] - need ["_build/page-" ++ takeBaseName dir ++ ".odoc" | dir <- docDirectories] - cmd_ (Cwd "_build") "odoc link page-_odoc.odoc -I ." - - "_odoc" "index.html" %> \out -> do - need ["_build/page-_odoc.odocl"] - cmd_ "odoc html-generate _build/page-_odoc.odocl --output-dir . --support-uri=_odoc --theme-uri=_odoc" - cmd_ "odoc support-files --output-dir _odoc" - - phony "odoc" $ do - need ["_odoc/index.html"] - need ["_odoc" takeBaseName dir "index.html" | dir <- docDirectories] - - "_build/*.odoc" %> \out -> do - let cmti = takeFileName out -<.> "cmti" - need ["_build" cmti] - let mli = takeFileName out -<.> "mli" - let parent = "page-" ++ case Map.lookup mli originalToMap of - Just original -> takeFileName $ takeDirectory original - Nothing -> error $ "No file matching \"" ++ mli ++ "\"" - need ["_build" parent -<.> "odoc"] - cmd_ (Cwd "_build") "odoc compile" cmti ("--parent=" ++ parent) "-I ." - - "_build/*.odocl" %> \out -> do - let mli = out -<.> "mli" - need [out -<.> "odoc"] - dep_mlis <- getModuleDeps $ ModuleDependencies mli - need ["_build" moduleToFile mli -<.> ".odoc" | mli <- dep_mlis] - cmd_ (Cwd "_build") "odoc link" (takeFileName out -<.> "odoc") "-I ." - - ["_build/*.cmi", "_build/*.cmti"] &%> \[out, annot] -> do - let mli = out -<.> "mli" - mli_dependencies <- getModuleDeps $ ModuleDependencies mli - need $ [mli] ++ ["_build" moduleToFile modul <.> "cmi" | modul <- mli_dependencies] - cmd_ (Cwd "_build") "ocamlfind ocamlopt -bin-annot -color=always -opaque -package " (intercalate "," ocamlfind_libraries) (takeFileName mli) "-o" (takeFileName out) - - "_build/*.ml" %> \out -> - case Map.lookup (dropDirectory1 out) originalToMap of - Just original -> copyFileChangedWithAnnotation original out - Nothing -> error $ "No file matching " ++ (dropDirectory1 out) - - ["_build/*.cmx", "_build/*.o"] &%> \[out, obj] -> do - let ml = out -<.> "ml" - mli_dependencies <- getModuleDeps $ ModuleDependencies ml - need $ [ml, out -<.> "cmi"] ++ ["_build" moduleToFile modul <.> "cmi" | modul <- mli_dependencies] - extra_flags <- askOracle $ ExtraFlags () - cmd_ (Cwd "_build") "ocamlfind ocamlopt -color=always -c -package" (intercalate "," ocamlfind_libraries) (takeFileName ml) "-o" (takeFileName out) extra_flags - - "_build/*.cmo" %> \out -> do - let ml = out -<.> "ml" - mli_dependencies <- getModuleDeps $ ModuleDependencies ml - need $ [ml, out -<.> "cmi"] ++ ["_build" moduleToFile modul <.> "cmi" | modul <- mli_dependencies] - extra_flags <- askOracle $ ExtraFlags () - cmd_ (Cwd "_build") "ocamlfind ocamlc -color=always -c -package" (intercalate "," ocamlfind_libraries) (takeFileName ml) "-o" (takeFileName out) extra_flags - - let implDeps file alreadySeen stack ext = do - let fileAsCmx = "_build" takeFileName file -<.> ext - if elem file stack then do - error $ "Cycle detected: " ++ (intercalate " " stack) ++ " " ++ file - else if elem fileAsCmx alreadySeen then do - return alreadySeen - else do - modules <- getModuleDeps $ ModuleDependencies ("_build" takeFileName file -<.> "ml") - let modules2 = ["_build" moduleToFile modul -<.> ext | modul <- modules] - let unseen = filter (\dep -> not $ elem (dep -<.> ext) alreadySeen) modules2 - let depsMl = ["_build" dep -<.> "ml" | dep <- unseen] - let mystack = stack ++ [file] - recursiveDeps <- foldM (\seen newfile -> do - recDeps <- implDeps newfile seen mystack ext - return recDeps) alreadySeen depsMl - return $ recursiveDeps ++ [fileAsCmx] - - let makeExecutable name main_file = do - "_bin" name %> \out -> do - let main_ml = "_build" main_file -<.> "ml" - let main_cmx = "_build" main_file -<.> "cmx" - absolute_out <- liftIO $ makeAbsolute out - deps <- implDeps main_ml [] [] "cmx" - let objs = [dep -<.> "o" | dep <- deps] - let reldeps = [takeFileName dep | dep <- deps] - need $ [main_cmx] ++ deps ++ objs - extra_flags <- askOracle $ ExtraFlags () - cmd_ (Cwd "_build") "ocamlfind ocamlopt -color=always -linkpkg -package" (intercalate "," $ ocamlfind_libraries ++ ["str", "unix"]) reldeps "-o" absolute_out extra_flags - return () - "_bin" name -<.> "byte" %> \out -> do - let main_ml = "_build" main_file -<.> "ml" - let main_cmx = "_build" main_file -<.> "cmo" - absolute_out <- liftIO $ makeAbsolute out - deps <- implDeps main_ml [] [] "cmo" - let reldeps = [takeFileName dep | dep <- deps] - need $ [main_cmx] ++ deps - extra_flags <- askOracle $ ExtraFlags () - cmd_ (Cwd "_build") "ocamlfind ocamlc -color=always -linkpkg -package" (intercalate "," $ ocamlfind_libraries ++ ["str", "unix"]) reldeps "-o" absolute_out extra_flags - return () - - let exes = [("chx86_make_lib_summary", "bCHXMakeLibSummary.ml"), - ("chx86_make_app_summary", "bCHXMakeAppSummary.ml"), - ("chx86_make_const_summary", "bCHXMakeConstSummary.ml"), - ("chx86_make_class_summary", "bCHXMakeClassSummary.ml"), - ("chx86_make_structdef", "bCHXMakeStructDefinition.ml"), - ("chx86_inspect_summaries", "bCHXInspectSummaries.ml"), - ("xanalyzer", "bCHXBinaryAnalyzer.ml"), - ("canalyzer", "cCHXCAnalyzer.ml"), - ("parseFile", "cCHXParseFile.ml"), - ("classinvariants", "jCHXClassInvariants.ml"), - ("translateclass", "jCHXTranslateClass.ml"), - ("usertemplate", "jCHXTemplate.ml"), - ("initialize", "jCHXInitializeAnalysis.ml"), - ("experiment", "jCHXClassExperiment.ml"), - ("template", "jCHXTemplate.ml"), - ("integrate", "jCHXIntegrateSummaries.ml"), - ("inspect", "jCHXInspectSummaries"), - ("native", "jCHXNativeMethodSignatures.ml"), - ("features", "jCHXExtractFeatures.ml"), - ("exprfeatures", "jCHXExtractExprFeatures.ml"), - ("poly", "jCHXClassPoly.ml"), - ("pattern", "jCHXCollectPatterns.ml")] - - let tests = [("xsimplifyTest", "xsimplifyTest.ml"), - ("xconsequenceTest", "xconsequenceTest.ml"), - ("bCHDoublewordTest", "bCHDoublewordTest.ml"), - ("bCHLocationTest", "bCHLocationTest.ml"), - ("bCHImmediateTest", "bCHImmediateTest.ml"), - ("bCHELFDebugAbbrevSectionTest", "bCHELFDebugAbbrevSectionTest.ml"), - ("bCHARMAssemblyFunctionTest", "bCHARMAssemblyFunctionTest.ml"), - ("bCHARMJumptableTest", "bCHARMJumptableTest.ml"), - ("bCHDisassembleARMInstructionTest", "bCHDisassembleARMInstructionTest.ml"), - ("bCHDisassembleThumbInstructionTest", "bCHDisassembleThumbInstructionTest.ml"), - ("bCHTranslateARMToCHIFTest", "bCHTranslateARMToCHIFTest.ml"), - ("bCHDisassemblePowerInstructionTest", "bCHDisassemblePowerInstructionTest.ml"), - ("bCHDisassembleVLEInstructionTest", "bCHDisassembleVLEInstructionTest.ml"), - ("bCHDwarfTest", "bCHDwarfTest.ml") - ] - - forM_ (exes ++ tests) (\pair -> do - let (name, main_file) = pair - makeExecutable name main_file) - - phony "binaries" $ do - -- warm ModuleDependencies cache - let files = [name | (name, original) <- Map.toList originalToMap] - let mls = filter (\file -> isInfixOf ".ml" file) files - askOracles [ModuleDependencies $ "_build" file | file <- mls] - -- actual dependencies - need ["_bin/" name | (name, _) <- exes ++ tests] - - phony "tests" $ do - forM_ tests (\(name, main_file) -> do - need ["_bin/" ++ name] - cmd_ ("_bin/" ++ name)) - - phony "bytecodes" $ do - -- warm ModuleDependencies cache - --let files = [name | (name, original) <- Map.toList originalToMap] - --let mls = filter (\file -> isInfixOf ".ml" file) files - --askOracles [ModuleDependencies $ "_build" file | file <- mls] - -- actual dependencies - need [("_bin/" name -<.> "byte") | (name, _) <- exes ++ tests] - - let makeDocs dir private = do - -- warm ModuleDependencies cache - let files = [name | (name, original) <- Map.toList originalToMap] - let mls = filter (\file -> isInfixOf ".ml" file) files - askOracles [ModuleDependencies $ "_build" file | file <- mls] - -- actual dependencies - let exe_files = ["_build" filename | (_, filename) <- exes ++ tests] - let foldCall accum file = do - recCall <- implDeps file (Set.toList accum) [] "cmx" - return $ Set.union accum $ Set.fromList recCall - allFiles <- foldM foldCall Set.empty exe_files - let relFiles = [takeFileName file | file <- Set.toList allFiles] - let full_mls = ["_build" file -<.> "ml" | file <- relFiles] - let full_mlis = ["_build" file -<.> "mli" | file <- relFiles] - let full_cmis = ["_build" file -<.> "cmi" | file <- relFiles] - let full_cmxs = ["_build" file -<.> "cmx" | file <- relFiles] - need (full_mls ++ full_mlis ++ full_cmis ++ full_cmxs) - let rel_mls = [file -<.> "ml" | file <- relFiles] - let rel_mlis = [file -<.> "mli" | file <- relFiles] - liftIO $ removeFiles dir ["//*"] - writeFile' (dir ".file") "q" - let filesToDoc = if private then rel_mls else (rel_mls ++ rel_mlis) - let workaround = [file | file <- filesToDoc, file /= "cCHReturnsite.ml", file /= "cCHCallsite.ml"] - cmd_ (Cwd "_build") "ocamlfind ocamldoc -keep-code -html -d " ("../" ++ dir) "-package" (intercalate "," $ ocamlfind_libraries ++ ["str","unix"]) workaround - - phony "docs_public" $ makeDocs "_docs_public" False - phony "docs_private" $ makeDocs "_docs_private" True - - want ["binaries"] diff --git a/CodeHawk/non_file_modules.txt b/CodeHawk/non_file_modules.txt deleted file mode 100644 index 5eac3bef..00000000 --- a/CodeHawk/non_file_modules.txt +++ /dev/null @@ -1,90 +0,0 @@ -Arg -Array -Big_int_Z -Buffer -Bytes -Callback -Cfg -Char -Cil -CostBoundCollections -Digest -DynArray -Errormsg -ExtArray -Extlib -ExtList -ExtString -FactorCollections -Filename -Frontc -GBin -GButton -Gc -Gdk -GdkEvent -GData -GDraw -GEdit -GFile -Glib -GMain -GMenu -GMisc -GnoCanvas -GObj -Gobject -GoblintCil -GPack -GRange -GSourceView2 -GText -GtkMisc -GtkPack -GToolbox -GTree -GWindow -Hashtbl -Int -Int32 -Int64 -IntCollections -IO -JTermCollections -JTermTableCollections -LanguageFactory -LargeFile -Lexing -List -Map -Marshal -NumericalCollections -Obj -Option -Pango -ParseError -Pervasives -Printexc -Printf -Q -Queue -Random -Result -Rmtmps -RmUnused -Scanf -Seq -Set -Stack -Stdlib -Str -String -StringCollections -StringMap -SymbolCollections -Sys -TaintNodeCollections -Unix -VariableCollections -Z -Zip diff --git a/newfile b/newfile deleted file mode 100644 index e69de29b..00000000 From affb898588d41bbf7dbd196ce501506754891100 Mon Sep 17 00:00:00 2001 From: Ben Karel Date: Thu, 8 May 2025 05:33:34 -0400 Subject: [PATCH 2/4] Standardize on dune build @install --- CodeHawk/README.md | 25 +++++++++---------------- 1 file changed, 9 insertions(+), 16 deletions(-) diff --git a/CodeHawk/README.md b/CodeHawk/README.md index ce91359e..11afe8f5 100644 --- a/CodeHawk/README.md +++ b/CodeHawk/README.md @@ -22,32 +22,25 @@ These commands should work for Ubuntu 22.04+: ``` sudo apt update -y -sudo apt install --no-install-recommends software-properties-common \ - build-essential unzip \ +sudo apt install --no-install-recommends \ + build-essential opam unzip openjdk-21-jdk \ pkg-config m4 zlib1g-dev libgmp-dev bubblewrap -y -# Run with sudo if you wish to install globally -bash -c "sh <(curl -fsSL https://opam.ocaml.org/install.sh)" opam init --bare git clone https://github.com/static-analysis-engineering/codehawk.git cd codehawk/CodeHawk -opam switch create . 5.2.0 && eval $(opam env) +opam switch create . 5.2.0 +eval $(opam env) opam install dune ocamlfind zarith camlzip extlib goblint-cil.2.0.6 -``` - -Depending on which analyzer you want to build: -- **Binary:** `dune build CHB` -- **C:** `dune build CHC` -- **Java:** `dune build CHJ` -- **all:** `dune build` -These targets can be combined, e.g. `dune build CHB CHC`. +dune build @install +``` The Makefiles in the repository are to help CodeHawk's developers debug circular module dependencies, they are not intended for users. Dependencies for other OS flavors: -- Arch Linux: `sudo pacman -Syu opam` -- Fedora: `sudo yum install opam diffutils zlib-devel ocaml-lablgtk-devel -y` -- macOS: `brew install opam` +- Arch Linux [untested]: `sudo pacman -Syu opam` +- Fedora [untested]: `sudo yum install opam diffutils zlib-devel -y` +- macOS [untested]: `brew install opam` From 5d6c98fa82ac1332769a4e4bedb0afd0b475aca2 Mon Sep 17 00:00:00 2001 From: Ben Karel Date: Sun, 18 May 2025 21:53:34 -0400 Subject: [PATCH 3/4] Address feedback from @Databean --- CodeHawk/README.md | 60 +++++++++++++++++++++++++++++----------------- 1 file changed, 38 insertions(+), 22 deletions(-) diff --git a/CodeHawk/README.md b/CodeHawk/README.md index 11afe8f5..79866b7a 100644 --- a/CodeHawk/README.md +++ b/CodeHawk/README.md @@ -1,31 +1,51 @@ -# Building with make +# Install Dependencies -## System Requirements +
+Ubuntu 22.04+ and Debian 11+ -Building codehawk requires the following applications and libraries: +``` +sudo apt update -y +sudo apt install --no-install-recommends \ + git ca-certificates \ + build-essential opam unzip default-jdk \ + pkg-config m4 zlib1g-dev libgmp-dev bubblewrap -y +``` +
-- Objective Caml (version 4.09 or higher) -- The Findlib / ocamlfind library manager -- The Zlib C library, version 1.1.3 or up -- The Zarith library -- goblint-cil, version 2.0.6 +
+Fedora -The CodeHawk Tool Suite contains three analyzers that can all be built -individually. All three analyzers have an optional gui that can be built -separately (and that requires additional dependencies to be installed). -The gui is current out-of-date and will require additional work to revive. +``` +sudo yum install awk diffutils git gmp-devel opam \ + perl-ExtUtils-MakeMaker perl-FindBin perl-Pod-Html zlib-devel -y +``` +
-### Install Dependencies: +
+Arch Linux -These commands should work for Ubuntu 22.04+: +``` +sudo pacman -Syu base-devel git opam +``` +
+ +
+macOS ``` -sudo apt update -y -sudo apt install --no-install-recommends \ - build-essential opam unzip openjdk-21-jdk \ - pkg-config m4 zlib1g-dev libgmp-dev bubblewrap -y +brew install opam +``` +
+ +# Build CodeHawk +Note that on Ubuntu 24.04 you must also pass `--disable-sandboxing` to `opam init`, +or create an AppArmor profile with `userns` permissions. This is also required +if you are running in `docker` without `--privileged`. +[Yes, this is a mess!](https://github.com/containers/bubblewrap/issues/505#issuecomment-2093203129) + +``` opam init --bare git clone https://github.com/static-analysis-engineering/codehawk.git @@ -40,7 +60,3 @@ dune build @install The Makefiles in the repository are to help CodeHawk's developers debug circular module dependencies, they are not intended for users. -Dependencies for other OS flavors: -- Arch Linux [untested]: `sudo pacman -Syu opam` -- Fedora [untested]: `sudo yum install opam diffutils zlib-devel -y` -- macOS [untested]: `brew install opam` From 25e2701072045d20e796f4e03c02937fb208f9de Mon Sep 17 00:00:00 2001 From: Ben Karel Date: Sun, 18 May 2025 21:58:57 -0400 Subject: [PATCH 4/4] Pin goblint-cil.2.0.6 in CI --- .github/workflows/dune.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/dune.yaml b/.github/workflows/dune.yaml index 99797757..55ceb5df 100644 --- a/.github/workflows/dune.yaml +++ b/.github/workflows/dune.yaml @@ -21,7 +21,7 @@ jobs: ocaml-compiler: ${{ matrix.ocaml-compiler }} - name: Install dependencies run: | - opam install extlib camlzip zarith ocamlbuild odoc goblint-cil + opam install extlib camlzip zarith ocamlbuild odoc goblint-cil.2.0.6 - name: Build executables run: eval $(opam env) && cd CodeHawk && dune build @install - name: Build documentation