/usr/bin/attack is in ladr4-apps 0.0.200911a-2.1build1.
This file is owned by root:root, with mode 0o755.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 | #!/usr/bin/python
# This script takes a Mace4 input file (the head) and a stream of
# candidates. It builds a list of models (M) of the candidates w.r.t.
# the clauses in the head.
#
# For each candidate C, if the C is true in any member of M,
# it is discarded; otherwise we look for a model of C and the
# clauses in the head; if a model is found, it is added to M and
# C is discarded; otherwise C is passed through to the standard output.
#
# Call it, for example, like this:
#
# attack head interps < candidates > candidates.out
#
# The file interps is created from scratch and must not exist at the start.
#
# The candidates must be one per line. A candidate need not be a single
# clause, e.g., it can be a pair of clauses. The important thing
# is that it makes sense when surrounded by "formulas(cand)." and
# "end_of_list." An exception: lines that start with "%" are treated
# as comment lines and are passed directly through to stdout.
import os
import sys
import re
import time
import socket
from subprocess import *
####################################
def runjob4(command_and_args, stdin_string=None):
if debug:
print "Starting job:", command_and_args
# Must have stdin arg; otherwise, it uses this process's stdin.
p1 = Popen(command_and_args, stdin=PIPE, stdout=PIPE, stderr=PIPE)
(out, err) = p1.communicate(stdin_string)
exit_code = p1.wait()
pid = p1.pid
if debug:
sys.stdout.writelines(out)
sys.stdout.writelines(err)
print "pid=%d, exit_code=%d" % (pid,exit_code)
return (pid, exit_code, out, err)
####################################
if len(sys.argv) != 3:
sys.stderr.write('need 2 args: head interp\n')
sys.exit(1)
head_fname = sys.argv[1]
interp_fname = sys.argv[2]
cand_fname = 'cand_%d.in' % os.getpid()
if os.path.isfile(interp_fname):
sys.stderr.write('file %s already exists\n' % interp_fname)
sys.exit(1)
interps = ""
checked = 0
passed = 0
num_interps = 0
debug = False
# assume these programs are in the user's path
mace4 = 'mace4'
get_interps = 'get_interps'
interpfilter = 'interpfilter'
mace4_model_exits = [0, 3, 4, 6]
mace4_error_exits = [1,102]
####################################
for line in sys.stdin:
if re.match('\s*%', line):
# passs comment line through to stdout
sys.stdout.write(line)
continue
cand = line
checked += 1
if checked % 100 == 0:
sys.stderr.write('checked %s\n' % checked)
interp_file = open(interp_fname, 'w')
interp_file.write('\nINTERMEDIATE RESULTS\n\n')
interp_file.writelines(interps)
interp_file.write('\nINTERMEDIATE RESULTS\n\n')
interp_file.close()
cand_file = open(cand_fname, 'w')
cand_file.write(cand)
cand_file.close()
(pid, rc, out, err) = runjob4([interpfilter, cand_fname, 'all_true'], interps)
if rc != 0: # not killed by existing model, so look for one with Mace4
cand_file = open(cand_fname, 'w')
cand_file.write('formulas(candidate).\n')
cand_file.write(cand)
cand_file.write('end_of_list.\n')
cand_file.close()
(pid, rc, out, err) = runjob4([mace4, '-f', head_fname, cand_fname])
if rc in mace4_error_exits:
sys.stderr.write('mace4 error %d\n' % rc)
elif rc in mace4_model_exits:
# candidate just killed; add interp to our aresenal of interps
num_interps += 1
(pid, rc, out, perr) = runjob4(get_interps, out)
line = '\n%% %s %% cand %d killed by\n\n' % (cand[:-1],checked)
interps = interps + line + out
else:
# candidate survives
passed += 1
line = '%s %% cand %d\n' % (cand[:-1],checked)
sys.stdout.write(line)
sys.stdout.flush()
os.remove(cand_fname)
date = time.strftime('%A, %b %d, %I:%M %p %Y', time.localtime())
host = socket.gethostname()
# Write the interp file.
interp_file = open(interp_fname, 'w')
interp_file.write('%% Started on %s at %s\n' % (host,date))
interp_file.write('%% Here is the head file %s.\n\n' % head_fname)
interp_file.write('%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n')
head_file = open(head_fname)
for line in head_file:
interp_file.write('%% %s' % line)
head_file.close()
interp_file.write('%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n')
interp_file.write(interps)
interp_file.write('\n%% Checked %d, passed %d, num_interps %d.\n' % (checked,passed,num_interps))
interp_file.write('%% Finished %s.\n' % date);
interp_file.close()
sys.stdout.write('%% attack4 %s %s (on %s): checked %d, passed %d, num_interps %d.\n' % \
(head_fname, interp_fname, host, checked, passed, num_interps))
sys.exit(0)
|