Skip to content

Commit a2de1be

Browse files
authored
Jt/limit opam jobs (#372)
* Add build-arg OPAM_JOBS to dockerfile * Update installation docs * Updated docs * Use nproc as default for OPAM_JOBS in Dockerfile * Update installation to include info about default OPAM_JOBS * Fix opam install . problem and allow docker build on branch
1 parent a492f1c commit a2de1be

File tree

41 files changed

+618
-267
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

41 files changed

+618
-267
lines changed

Dockerfile

+10-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,14 @@
11
FROM ocaml/opam:ubuntu-20.04-ocaml-4.14
22

3+
ARG OPAM_JOBS=0
4+
ARG BRANCH=master
5+
6+
RUN if [ "${OPAM_JOBS}" -eq "0" ]; then \
7+
sed -i 's/jobs: [[:digit:]]\+/jobs: '$(nproc)'/' /home/opam/.opam/config; \
8+
else \
9+
sed -i 's/jobs: [[:digit:]]\+/jobs: '${OPAM_JOBS}'/' /home/opam/.opam/config; \
10+
fi
11+
312
RUN sudo -E apt update; \
413
sudo -E apt install -qq -yy \
514
zip binutils-multiarch clang debianutils libgmp-dev \
@@ -17,7 +26,7 @@ RUN cd bap-toolkit; \
1726
opam config exec -- make; \
1827
opam config exec -- make install
1928

20-
RUN git clone https://github.com/draperlaboratory/cbat_tools.git
29+
RUN git clone --branch "${BRANCH}" https://github.com/draperlaboratory/cbat_tools.git
2130

2231
RUN cd cbat_tools/wp; \
2332
opam config exec -- make

docs/doc/html/bap_wp/Bap_wp/Bil_to_bir/index.html

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
<!DOCTYPE html>
2-
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Bil_to_bir (bap_wp.Bap_wp.Bil_to_bir)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a><a href="../../index.html">bap_wp</a> &#x00BB; <a href="../index.html">Bap_wp</a> &#x00BB; Bil_to_bir</nav><h1>Module <code>Bap_wp.Bil_to_bir</code></h1></header><aside><p>This module provides utilities to translate from a BIL <span class="xref-unresolved" title="unresolved reference to &quot;Bap.Std.Bil.t&quot;"><span class="xref-unresolved" title="unresolved reference to &quot;Bap.Std.Bil&quot;"><span class="xref-unresolved" title="unresolved reference to &quot;Bap.Std&quot;"><code>Bap</code>.Std</span>.Bil</span>.t</span> expression to a BIR subroutine, for which we can then invoke <a href="../Precondition/index.html#val-visit_sub"><code>Precondition.visit_sub</code></a> to get the weakest precondition.</p><p>This enables using the clean BIL embedded DSL syntax, e.g.</p><pre><code class="ml">Bil.([
2+
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Bil_to_bir (bap_wp.Bap_wp.Bil_to_bir)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.1.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a><a href="../../index.html">bap_wp</a> &#x00BB; <a href="../index.html">Bap_wp</a> &#x00BB; Bil_to_bir</nav><header class="odoc-preamble"><h1>Module <code><span>Bap_wp.Bil_to_bir</span></code></h1><p>This module provides utilities to translate from a BIL <code>Bil</code>.t expression to a BIR subroutine, for which we can then invoke <a href="../Precondition/index.html#val-visit_sub"><code>Precondition.visit_sub</code></a> to get the weakest precondition.</p><p>This enables using the clean BIL embedded DSL syntax, e.g.</p><pre><code>Bil.([
33
v := src lsr i32 1;
44
r := src;
55
s := i32 31;
@@ -10,4 +10,4 @@
1010
s := var s - i32 1;
1111
];
1212
dst := var r lsl var s;
13-
]) |&gt; bil_to_sub</code></pre><p>As in the BAP documentation, to build subroutines.</p></aside><dl><dt class="spec value" id="val-mk_assert_fail"><a href="#val-mk_assert_fail" class="anchor"></a><code><span class="keyword">val</span> mk_assert_fail : unit <span>&#45;&gt;</span> Bap.Std.Sub.t * Bap.Std.Exp.t</code></dt><dd><p>Create a pair of a subroutine with name <code>__assert_fail</code> and an expression which represents an invocation of that subroutine.</p><p>A subsequent call to <a href="index.html#val-bil_to_sub"><code>bil_to_sub</code></a> will correctly translate that expression to a BIR <code>call</code> expression.</p></dd></dl><dl><dt class="spec value" id="val-bil_to_sub"><a href="#val-bil_to_sub" class="anchor"></a><code><span class="keyword">val</span> bil_to_sub : Bap.Std.Bil.t <span>&#45;&gt;</span> Bap.Std.Sub.t</code></dt><dd><p>Take a BIL program (a list of statements) and turn it into a subroutine.</p></dd></dl></div></body></html>
13+
]) |&gt; bil_to_sub</code></pre><p>As in the BAP documentation, to build subroutines.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value" id="val-mk_assert_fail" class="anchored"><a href="#val-mk_assert_fail" class="anchor"></a><code><span><span class="keyword">val</span> mk_assert_fail : <span>unit <span class="arrow">&#45;&gt;</span></span> <span><span class="xref-unresolved">Bap</span>.Std.sub <span class="xref-unresolved">Bap</span>.Std.term</span> * <span class="xref-unresolved">Bap</span>.Std.exp</span></code></div><div class="spec-doc"><p>Create a pair of a subroutine with name <code>__assert_fail</code> and an expression which represents an invocation of that subroutine.</p><p>A subsequent call to <a href="#val-bil_to_sub"><code>bil_to_sub</code></a> will correctly translate that expression to a BIR <code>call</code> expression.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-bil_to_sub" class="anchored"><a href="#val-bil_to_sub" class="anchor"></a><code><span><span class="keyword">val</span> bil_to_sub : <span><span class="xref-unresolved">Bap</span>.Std.bil <span class="arrow">&#45;&gt;</span></span> <span><span class="xref-unresolved">Bap</span>.Std.sub <span class="xref-unresolved">Bap</span>.Std.term</span></span></code></div><div class="spec-doc"><p>Take a BIL program (a list of statements) and turn it into a subroutine.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-call" class="anchored"><a href="#val-call" class="anchor"></a><code><span><span class="keyword">val</span> call : <span><span><span class="xref-unresolved">Bap</span>.Std.sub <span class="xref-unresolved">Bap</span>.Std.term</span> <span class="arrow">&#45;&gt;</span></span> <span><span class="xref-unresolved">Bap</span>.Std.typ <span class="arrow">&#45;&gt;</span></span> <span class="xref-unresolved">Bap</span>.Std.Bil.Types.stmt</span></code></div><div class="spec-doc"><p>Take a <code>sub term</code> and a type for the term to build a BIL function-call</p></div></div></div></body></html>

0 commit comments

Comments
 (0)