ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions | Variables
mainReal.c File Reference
#include <sys/time.h>
#include <sys/times.h>
#include <sys/resource.h>
#include <unistd.h>
#include <signal.h>
#include <stdlib.h>
#include "base/abc/abc.h"
#include "mainInt.h"
#include "base/wlc/wlc.h"
Include dependency graph for mainReal.c:

Go to the source code of this file.

Functions

int Abc_RealMain (int argc, char *argv[])
 

Variables

unsigned enable_dbg_outs = 1
 FUNCTION DEFINITIONS ///.
 

Function Documentation

◆ Abc_RealMain()

int Abc_RealMain ( int argc,
char * argv[] )

Function*************************************************************

Synopsis [The main() procedure.]

Description []

SideEffects []

SeeAlso []

Definition at line 88 of file mainReal.c.

89{
90 Abc_Frame_t * pAbc;
91 Vec_Str_t* sCommandUsr = Vec_StrAlloc(1000);
92 char sCommandTmp[ABC_MAX_STR], sReadCmd[1000], sWriteCmd[1000];
93 const char * sOutFile, * sInFile;
94 char * sCommand;
95 int fStatus = 0;
96 int c, fInitSource, fInitRead, fFinalWrite;
97
98 enum {
99 INTERACTIVE, // interactive mode
100 BATCH, // batch mode, run a command and quit
101 BATCH_THEN_INTERACTIVE, // run a command, then back to interactive mode
102 BATCH_QUIET, // as in batch mode, but don't echo the command
103 BATCH_QUIET_THEN_INTERACTIVE, // as in batch then interactive mode, but don't echo the command
104 BATCH_SMT // special batch mode, which expends SMTLIB problem via stdin
105 } fBatch;
106
107 // added to detect memory leaks
108 // watch for {,,msvcrtd.dll}*__p__crtBreakAlloc()
109 // (http://support.microsoft.com/kb/151585)
110#if defined(_DEBUG) && defined(_MSC_VER)
111 _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
112#endif
113
114 // get global frame (singleton pattern)
115 // will be initialized on first call
116 pAbc = Abc_FrameGetGlobalFrame();
117 pAbc->sBinary = argv[0];
118
119 // default options
120 fBatch = INTERACTIVE;
121 fInitSource = 1;
122 fInitRead = 0;
123 fFinalWrite = 0;
124 sInFile = sOutFile = NULL;
125 sprintf( sReadCmd, "read" );
126 sprintf( sWriteCmd, "write" );
127
128 Extra_UtilGetoptReset();
129 while ((c = Extra_UtilGetopt(argc, argv, "dm:l:c:q:C:Q:S:hf:F:o:st:T:xb")) != EOF) {
130 switch(c) {
131
132 case 'd':
133 enable_dbg_outs ^= 1;
134 break;
135
136 case 'm': {
137#if !defined(WIN32) && !defined(ABC_NO_RLIMIT)
138 int maxMb = atoi(globalUtilOptarg);
139 printf("Limiting memory use to %d MB\n", maxMb);
140 struct rlimit limit = {
141 maxMb * (1llu << 20), /* soft limit */
142 maxMb * (1llu << 20) /* hard limit */
143 };
144 setrlimit(RLIMIT_AS, &limit);
145#endif
146 break;
147 }
148 case 'l': {
149#if !defined(WIN32) && !defined(ABC_NO_RLIMIT)
150 rlim_t maxTime = atoi(globalUtilOptarg);
151 printf("Limiting time to %d seconds\n", (int)maxTime);
152 struct rlimit limit = {
153 maxTime, /* soft limit */
154 maxTime /* hard limit */
155 };
156 setrlimit(RLIMIT_CPU, &limit);
157#endif
158 break;
159 }
160 case 'c':
161 if( Vec_StrSize(sCommandUsr) > 0 )
162 {
163 Vec_StrAppend(sCommandUsr, " ; ");
164 }
165 Vec_StrAppend(sCommandUsr, globalUtilOptarg );
166 fBatch = BATCH;
167 break;
168
169 case 'q':
170 if( Vec_StrSize(sCommandUsr) > 0 )
171 {
172 Vec_StrAppend(sCommandUsr, " ; ");
173 }
174 Vec_StrAppend(sCommandUsr, globalUtilOptarg );
175 fBatch = BATCH_QUIET;
176 break;
177
178 case 'Q':
179 if( Vec_StrSize(sCommandUsr) > 0 )
180 {
181 Vec_StrAppend(sCommandUsr, " ; ");
182 }
183 Vec_StrAppend(sCommandUsr, globalUtilOptarg );
184 fBatch = BATCH_QUIET_THEN_INTERACTIVE;
185 break;
186
187 case 'C':
188 if( Vec_StrSize(sCommandUsr) > 0 )
189 {
190 Vec_StrAppend(sCommandUsr, " ; ");
191 }
192 Vec_StrAppend(sCommandUsr, globalUtilOptarg );
193 fBatch = BATCH_THEN_INTERACTIVE;
194 break;
195
196 case 'S':
197 if( Vec_StrSize(sCommandUsr) > 0 )
198 {
199 Vec_StrAppend(sCommandUsr, " ; ");
200 }
201 Vec_StrAppend(sCommandUsr, globalUtilOptarg );
202 fBatch = BATCH_SMT;
203 break;
204
205 case 'f':
206 if( Vec_StrSize(sCommandUsr) > 0 )
207 {
208 Vec_StrAppend(sCommandUsr, " ; ");
209 }
210 Vec_StrPrintF(sCommandUsr, "source %s", globalUtilOptarg );
211 fBatch = BATCH;
212 break;
213
214 case 'F':
215 if( Vec_StrSize(sCommandUsr) > 0 )
216 {
217 Vec_StrAppend(sCommandUsr, " ; ");
218 }
219 Vec_StrPrintF(sCommandUsr, "source -x %s", globalUtilOptarg );
220 fBatch = BATCH;
221 break;
222
223 case 'h':
224 goto usage;
225 break;
226
227 case 'o':
228 sOutFile = globalUtilOptarg;
229 fFinalWrite = 1;
230 break;
231
232 case 's':
233 fInitSource = 0;
234 break;
235
236 case 't':
237 if ( TypeCheck( pAbc, globalUtilOptarg ) )
238 {
239 if ( (!strcmp(globalUtilOptarg, "none")) == 0 )
240 {
241 fInitRead = 1;
242 sprintf( sReadCmd, "read_%s", globalUtilOptarg );
243 }
244 }
245 else {
246 goto usage;
247 }
248 fBatch = BATCH;
249 break;
250
251 case 'T':
252 if ( TypeCheck( pAbc, globalUtilOptarg ) )
253 {
254 if ( (!strcmp(globalUtilOptarg, "none")) == 0)
255 {
256 fFinalWrite = 1;
257 sprintf( sWriteCmd, "write_%s", globalUtilOptarg);
258 }
259 }
260 else {
261 goto usage;
262 }
263 fBatch = BATCH;
264 break;
265
266 case 'x':
267 fFinalWrite = 0;
268 fInitRead = 0;
269 fBatch = BATCH;
270 break;
271
272 case 'b':
273 Abc_FrameSetBridgeMode();
274 break;
275
276 default:
277 goto usage;
278 }
279 }
280
281 Vec_StrPush(sCommandUsr, '\0');
282
283 if ( fBatch == BATCH_SMT )
284 {
285 Wlc_StdinProcessSmt( pAbc, Vec_StrArray(sCommandUsr) );
286 Abc_Stop();
287 return 0;
288 }
289
290 if ( Abc_FrameIsBridgeMode() )
291 {
292 extern Gia_Man_t * Gia_ManFromBridge( FILE * pFile, Vec_Int_t ** pvInit );
293 pAbc->pGia = Gia_ManFromBridge( stdin, NULL );
294 }
295 else if ( fBatch!=INTERACTIVE && fBatch!=BATCH_QUIET && fBatch!=BATCH_QUIET_THEN_INTERACTIVE && Vec_StrSize(sCommandUsr)>0 )
296 Abc_Print( 1, "ABC command line: \"%s\".\n\n", Vec_StrArray(sCommandUsr) );
297
298 if ( fBatch!=INTERACTIVE )
299 {
300 pAbc->fBatchMode = 1;
301
302 if (argc - globalUtilOptind == 0)
303 {
304 sInFile = NULL;
305 }
306 else if (argc - globalUtilOptind == 1)
307 {
308 fInitRead = 1;
309 sInFile = argv[globalUtilOptind];
310 }
311 else
312 {
313 Abc_UtilsPrintUsage( pAbc, argv[0] );
314 }
315
316 // source the resource file
317 if ( fInitSource )
318 {
319 Abc_UtilsSource( pAbc );
320 }
321
322 fStatus = 0;
323 if ( fInitRead && sInFile )
324 {
325 sprintf( sCommandTmp, "%s %s", sReadCmd, sInFile );
326 fStatus = Cmd_CommandExecute( pAbc, sCommandTmp );
327 }
328
329 if ( fStatus == 0 )
330 {
331 /* cmd line contains `source <file>' */
332 fStatus = Cmd_CommandExecute( pAbc, Vec_StrArray(sCommandUsr) );
333 if ( (fStatus == 0 || fStatus == -1) && fFinalWrite && sOutFile )
334 {
335 sprintf( sCommandTmp, "%s %s", sWriteCmd, sOutFile );
336 fStatus = Cmd_CommandExecute( pAbc, sCommandTmp );
337 }
338 }
339
340 if (fBatch == BATCH_THEN_INTERACTIVE || fBatch == BATCH_QUIET_THEN_INTERACTIVE){
341 fBatch = INTERACTIVE;
342 pAbc->fBatchMode = 0;
343 }
344 }
345
346 Vec_StrFreeP(&sCommandUsr);
347
348 if ( fBatch==INTERACTIVE )
349 {
350 // start interactive mode
351
352 // print the hello line
353 Abc_UtilsPrintHello( pAbc );
354 // print history of the recent commands
355 Cmd_HistoryPrint( pAbc, 10 );
356
357 // source the resource file
358 if ( fInitSource )
359 {
360 Abc_UtilsSource( pAbc );
361 }
362
363 // execute commands given by the user
364 while ( !feof(stdin) )
365 {
366 // print command line prompt and
367 // get the command from the user
368 sCommand = Abc_UtilsGetUsersInput( pAbc );
369
370 // execute the user's command
371 fStatus = Cmd_CommandExecute( pAbc, sCommand );
372
373 // stop if the user quitted or an error occurred
374 if ( fStatus == -1 || fStatus == -2 )
375 break;
376 }
377 }
378
379 // if the memory should be freed, quit packages
380// if ( fStatus < 0 )
381 {
382 Abc_Stop();
383 }
384 return 0;
385
386usage:
387 Abc_UtilsPrintHello( pAbc );
388 Abc_UtilsPrintUsage( pAbc, argv[0] );
389 return 1;
390}
Abc_Frame_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Frame_t_ Abc_Frame_t
INCLUDES ///.
Definition abcapis.h:38
Abc_Stop
ABC_DLL void Abc_Stop()
Definition mainLib.c:76
Abc_FrameGetGlobalFrame
ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame()
Definition mainFrame.c:643
Abc_FrameSetBridgeMode
ABC_DLL void Abc_FrameSetBridgeMode()
Definition mainFrame.c:114
Abc_FrameIsBridgeMode
ABC_DLL int Abc_FrameIsBridgeMode()
Definition mainFrame.c:113
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Vec_Str_t
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
Cmd_HistoryPrint
void Cmd_HistoryPrint(Abc_Frame_t *p, int Limit)
Definition cmdHist.c:164
Cmd_CommandExecute
ABC_DLL int Cmd_CommandExecute(Abc_Frame_t *pAbc, const char *sCommand)
Definition cmdApi.c:193
globalUtilOptind
int globalUtilOptind
Definition extraUtilUtil.c:45
globalUtilOptarg
const char * globalUtilOptarg
Definition extraUtilUtil.c:44
Extra_UtilGetopt
int Extra_UtilGetopt(int argc, char *argv[], const char *optstring)
Definition extraUtilUtil.c:98
Extra_UtilGetoptReset
ABC_DLL void Extra_UtilGetoptReset()
Definition extraUtilUtil.c:80
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Abc_UtilsPrintUsage
ABC_DLL void Abc_UtilsPrintUsage(Abc_Frame_t *pAbc, char *ProgName)
Definition mainUtils.c:127
ABC_MAX_STR
#define ABC_MAX_STR
Definition mainInt.h:52
Abc_UtilsPrintHello
ABC_DLL void Abc_UtilsPrintHello(Abc_Frame_t *pAbc)
Definition mainUtils.c:111
Abc_UtilsSource
ABC_DLL void Abc_UtilsSource(Abc_Frame_t *pAbc)
Definition mainUtils.c:160
Abc_UtilsGetUsersInput
ABC_DLL char * Abc_UtilsGetUsersInput(Abc_Frame_t *pAbc)
Definition mainUtils.c:77
enable_dbg_outs
unsigned enable_dbg_outs
FUNCTION DEFINITIONS ///.
Definition mainReal.c:75
usage
usage()
Definition main.c:626
Gia_ManFromBridge
Gia_Man_t * Gia_ManFromBridge(FILE *pFile, Vec_Int_t **pvInit)
Definition utilBridge.c:471
strcmp
int strcmp()
sprintf
char * sprintf()
Wlc_StdinProcessSmt
int Wlc_StdinProcessSmt(Abc_Frame_t *pAbc, char *pCmd)
Definition wlcStdin.c:190
Here is the call graph for this function:
Here is the caller graph for this function:

Variable Documentation

◆ enable_dbg_outs

unsigned enable_dbg_outs = 1

FUNCTION DEFINITIONS ///.

Definition at line 75 of file mainReal.c.